src/HOL/Lazy_Sequence.thy
changeset 56643 41d3596d8a64
parent 55642 63beb38e9258
child 56846 9df717fef2bb
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Apr 23 10:23:26 2014 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 23 10:23:27 2014 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    by (auto intro: lazy_sequence_eqI)
     1.5  
     1.6  lemma lazy_sequence_size_eq:
     1.7 -  "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
     1.8 +  "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
     1.9    by (cases xq) simp
    1.10  
    1.11  lemma size_lazy_sequence_eq [code]: