src/HOL/Lazy_Sequence.thy
changeset 55642 63beb38e9258
parent 55466 786edc984c98
child 56643 41d3596d8a64
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -52,8 +52,8 @@
     1.4  code_datatype Lazy_Sequence
     1.5  
     1.6  declare list_of_lazy_sequence.simps [code del]
     1.7 -declare lazy_sequence.cases [code del]
     1.8 -declare lazy_sequence.recs [code del]
     1.9 +declare lazy_sequence.case [code del]
    1.10 +declare lazy_sequence.rec [code del]
    1.11  
    1.12  lemma list_of_Lazy_Sequence [simp]:
    1.13    "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of