src/HOLCF/ex/Stream.thy
changeset 35642 f478d5a9d238
parent 35557 5da670d57118
child 35781 b7738ab762b1
     1.1 --- a/src/HOLCF/ex/Stream.thy	Sun Mar 07 16:12:01 2010 -0800
     1.2 +++ b/src/HOLCF/ex/Stream.thy	Sun Mar 07 16:39:31 2010 -0800
     1.3 @@ -845,7 +845,7 @@
     1.4  by blast+
     1.5  
     1.6  lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
     1.7 -by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast)
     1.8 +by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast)
     1.9  
    1.10  (* ----------------------------------------------------------------------- *)
    1.11     subsection "finiteness"
    1.12 @@ -912,7 +912,7 @@
    1.13     apply (simp+,rule slen_take_lemma3 [of _ s1 s2])
    1.14    apply (simp+,rule_tac x="UU" in exI)
    1.15  apply (insert slen_take_lemma3 [of _ s1 s2])
    1.16 -by (rule stream.take_lemmas,simp)
    1.17 +by (rule stream.take_lemma,simp)
    1.18  
    1.19  (* ----------------------------------------------------------------------- *)
    1.20     subsection "continuity"