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