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)
```