src/HOLCF/IOA/meta_theory/Sequence.thy
changeset 35642 f478d5a9d238
parent 35532 60647586b173
child 35781 b7738ab762b1
     1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Mar 07 16:12:01 2010 -0800
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Mar 07 16:39:31 2010 -0800
     1.3 @@ -850,7 +850,7 @@
     1.4  
     1.5  lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
     1.6  apply (rule iffI)
     1.7 -apply (rule seq.take_lemmas)
     1.8 +apply (rule seq.take_lemma)
     1.9  apply auto
    1.10  done
    1.11  
    1.12 @@ -936,7 +936,7 @@
    1.13                 ==> A x --> (f x)=(g x)"
    1.14  apply (case_tac "Forall Q x")
    1.15  apply (auto dest!: divide_Seq3)
    1.16 -apply (rule seq.take_lemmas)
    1.17 +apply (rule seq.take_lemma)
    1.18  apply auto
    1.19  done
    1.20  
    1.21 @@ -957,7 +957,7 @@
    1.22                                = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
    1.23                 ==> A x --> (f x)=(g x)"
    1.24  apply (rule impI)
    1.25 -apply (rule seq.take_lemmas)
    1.26 +apply (rule seq.take_lemma)
    1.27  apply (rule mp)
    1.28  prefer 2 apply assumption
    1.29  apply (rule_tac x="x" in spec)
    1.30 @@ -978,7 +978,7 @@
    1.31                                = seq_take n$(g (s1 @@ y>>s2)) |]
    1.32                 ==> A x --> (f x)=(g x)"
    1.33  apply (rule impI)
    1.34 -apply (rule seq.take_lemmas)
    1.35 +apply (rule seq.take_lemma)
    1.36  apply (rule mp)
    1.37  prefer 2 apply assumption
    1.38  apply (rule_tac x="x" in spec)
    1.39 @@ -1000,7 +1000,7 @@
    1.40                           = seq_take (Suc n)$(g (y>>s)) |]
    1.41                 ==> A x --> (f x)=(g x)"
    1.42  apply (rule impI)
    1.43 -apply (rule seq.take_lemmas)
    1.44 +apply (rule seq.take_lemma)
    1.45  apply (rule mp)
    1.46  prefer 2 apply assumption
    1.47  apply (rule_tac x="x" in spec)