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/Lazy_Sequence.thy
changeset 56643 41d3596d8a64
parent 55642 63beb38e9258
child 56846 9df717fef2bb 
--- a/src/HOL/Lazy_Sequence.thy	Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 23 10:23:27 2014 +0200
@@ -28,7 +28,7 @@
   by (auto intro: lazy_sequence_eqI)
 
 lemma lazy_sequence_size_eq:
-  "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
+  "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
   by (cases xq) simp
 
 lemma size_lazy_sequence_eq [code]:
isabelle