From 8d108b98ee40f1f728e66efc53e4a180d5b63890 Mon Sep 17 00:00:00 2001 From: Ankit Kachroo Date: Sat, 27 Oct 2018 17:11:48 +0530 Subject: [PATCH] Update proving.md Changed IVy spell presentation on line #351 --- doc/proving.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/proving.md b/doc/proving.md index edcca0e93..2ae29bea0 100644 --- a/doc/proving.md +++ b/doc/proving.md @@ -348,7 +348,7 @@ expressing the transitivity of equality: ``` We don't need a proof for this, since the `auto` tactic can handle -it. The verification condition that ivy generates is: +it. The verification condition that IVy generates is: # X = Y & Y = Z -> X = Z