src/HOLCF/IOA/meta_theory/CompoTraces.thy
changeset 35642 f478d5a9d238
parent 35215 a03462cbf86f
child 36543 0e7fc5bf38de
     1.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Mar 07 16:12:01 2010 -0800
     1.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sun Mar 07 16:39:31 2010 -0800
     1.3 @@ -467,7 +467,7 @@
     1.4    LastActExtsch A schA & LastActExtsch B schB   
     1.5    --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
     1.6  apply (intro strip)
     1.7 -apply (rule seq.take_lemmas)
     1.8 +apply (rule seq.take_lemma)
     1.9  apply (rule mp)
    1.10  prefer 2 apply assumption
    1.11  back back back back
    1.12 @@ -687,7 +687,7 @@
    1.13    LastActExtsch A schA & LastActExtsch B schB   
    1.14    --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
    1.15  apply (intro strip)
    1.16 -apply (rule seq.take_lemmas)
    1.17 +apply (rule seq.take_lemma)
    1.18  apply (rule mp)
    1.19  prefer 2 apply assumption
    1.20  back back back back