From f28fa68497352ffb57ab2846da4cc1c1aeaf1968 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 12 Aug 2015 22:44:50 -0700
Subject: Change the induction heuristic for lemmas to also look in
 precondition for clues about which parameters to include. As a result,
 improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and
 beautified some others.

---
 Test/dafny4/KozenSilva.dfy.expect | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/dafny4/KozenSilva.dfy.expect')

diff --git a/Test/dafny4/KozenSilva.dfy.expect b/Test/dafny4/KozenSilva.dfy.expect
index c6c90498..90432af3 100644
--- a/Test/dafny4/KozenSilva.dfy.expect
+++ b/Test/dafny4/KozenSilva.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 47 verified, 0 errors
+Dafny program verifier finished with 49 verified, 0 errors
-- 
cgit v1.2.3