src/HOLCF/IOA/meta_theory/CompoTraces.thy
changeset 10835 f4745d77e620
parent 3842 b55686a7b22c
child 12028 52aa183c15bb
     1.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  defs
     1.5  
     1.6  mksch_def
     1.7 -  "mksch A B == (fix`(LAM h tr schA schB. case tr of 
     1.8 +  "mksch A B == (fix$(LAM h tr schA schB. case tr of 
     1.9         nil => nil
    1.10      | x##xs => 
    1.11        (case x of 
    1.12 @@ -25,24 +25,24 @@
    1.13        | Def y => 
    1.14           (if y:act A then 
    1.15               (if y:act B then 
    1.16 -                   ((Takewhile (%a. a:int A)`schA)
    1.17 -                      @@ (Takewhile (%a. a:int B)`schB)
    1.18 -                           @@ (y>>(h`xs
    1.19 -                                    `(TL`(Dropwhile (%a. a:int A)`schA))
    1.20 -                                    `(TL`(Dropwhile (%a. a:int B)`schB))
    1.21 +                   ((Takewhile (%a. a:int A)$schA)
    1.22 +                      @@ (Takewhile (%a. a:int B)$schB)
    1.23 +                           @@ (y>>(h$xs
    1.24 +                                    $(TL$(Dropwhile (%a. a:int A)$schA))
    1.25 +                                    $(TL$(Dropwhile (%a. a:int B)$schB))
    1.26                      )))
    1.27                else
    1.28 -                 ((Takewhile (%a. a:int A)`schA)
    1.29 -                  @@ (y>>(h`xs
    1.30 -                           `(TL`(Dropwhile (%a. a:int A)`schA))
    1.31 -                           `schB)))
    1.32 +                 ((Takewhile (%a. a:int A)$schA)
    1.33 +                  @@ (y>>(h$xs
    1.34 +                           $(TL$(Dropwhile (%a. a:int A)$schA))
    1.35 +                           $schB)))
    1.36                )
    1.37            else 
    1.38               (if y:act B then 
    1.39 -                 ((Takewhile (%a. a:int B)`schB)
    1.40 -                     @@ (y>>(h`xs
    1.41 -                              `schA
    1.42 -                              `(TL`(Dropwhile (%a. a:int B)`schB))
    1.43 +                 ((Takewhile (%a. a:int B)$schB)
    1.44 +                     @@ (y>>(h$xs
    1.45 +                              $schA
    1.46 +                              $(TL$(Dropwhile (%a. a:int B)$schB))
    1.47                                )))
    1.48               else
    1.49                 UU
    1.50 @@ -56,8 +56,8 @@
    1.51         let trA = fst TracesA; sigA = snd TracesA; 
    1.52             trB = fst TracesB; sigB = snd TracesB       
    1.53         in
    1.54 -       (    {tr. Filter (%a. a:actions sigA)`tr : trA}
    1.55 -        Int {tr. Filter (%a. a:actions sigB)`tr : trB}
    1.56 +       (    {tr. Filter (%a. a:actions sigA)$tr : trA}
    1.57 +        Int {tr. Filter (%a. a:actions sigB)$tr : trB}
    1.58          Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
    1.59          asig_comp sigA sigB)"
    1.60  
    1.61 @@ -65,7 +65,7 @@
    1.62  
    1.63  
    1.64  finiteR_mksch
    1.65 -  "Finite (mksch A B`tr`x`y) --> Finite tr"
    1.66 +  "Finite (mksch A B$tr$x$y) --> Finite tr"
    1.67  
    1.68  
    1.69