src/HOL/Lazy_Sequence.thy
changeset 55416 dd7992d4a61a
parent 55413 a8e96847523c
child 55466 786edc984c98
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -35,12 +35,12 @@
     1.4    "size (xq :: 'a lazy_sequence) = 0"
     1.5    by (cases xq) simp
     1.6  
     1.7 -lemma lazy_sequence_case [simp]:
     1.8 -  "lazy_sequence_case f xq = f (list_of_lazy_sequence xq)"
     1.9 +lemma case_lazy_sequence [simp]:
    1.10 +  "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    1.11    by (cases xq) auto
    1.12  
    1.13 -lemma lazy_sequence_rec [simp]:
    1.14 -  "lazy_sequence_rec f xq = f (list_of_lazy_sequence xq)"
    1.15 +lemma rec_lazy_sequence [simp]:
    1.16 +  "rec_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
    1.17    by (cases xq) auto
    1.18  
    1.19  definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
    1.20 @@ -346,4 +346,3 @@
    1.21    if_seq_def those_def not_seq_def product_def 
    1.22  
    1.23  end
    1.24 -