Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Examples/Stream.thy
changeset 51779 273e7a90b167
parent 51778 190f89980f7b
child 51788 5fe72280a49f 
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Apr 25 17:13:24 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Apr 25 17:25:10 2013 +0200
@@ -197,7 +197,7 @@
 proof
   assume ?R
   thus ?L 
-    by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = smap f (sdrop n s) \<and> s2 = sdrop n s'"])
+    by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = smap f (sdrop n s) \<and> s2 = sdrop n s'", consumes 0])
       (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
 qed auto
isabelle