src/HOLCF/IOA/meta_theory/CompoTraces.thy

--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -17,7 +17,7 @@
 defs
 
 mksch_def
-  "mksch A B == (fix`(LAM h tr schA schB. case tr of 
+  "mksch A B == (fix$(LAM h tr schA schB. case tr of 
        nil => nil
     | x##xs => 
       (case x of 
@@ -25,24 +25,24 @@
       | Def y => 
          (if y:act A then 
              (if y:act B then 
-                   ((Takewhile (%a. a:int A)`schA)
-                      @@ (Takewhile (%a. a:int B)`schB)
-                           @@ (y>>(h`xs
-                                    `(TL`(Dropwhile (%a. a:int A)`schA))
-                                    `(TL`(Dropwhile (%a. a:int B)`schB))
+                   ((Takewhile (%a. a:int A)$schA)
+                      @@ (Takewhile (%a. a:int B)$schB)
+                           @@ (y>>(h$xs
+                                    $(TL$(Dropwhile (%a. a:int A)$schA))
+                                    $(TL$(Dropwhile (%a. a:int B)$schB))
                     )))
               else
-                 ((Takewhile (%a. a:int A)`schA)
-                  @@ (y>>(h`xs
-                           `(TL`(Dropwhile (%a. a:int A)`schA))
-                           `schB)))
+                 ((Takewhile (%a. a:int A)$schA)
+                  @@ (y>>(h$xs
+                           $(TL$(Dropwhile (%a. a:int A)$schA))
+                           $schB)))
               )
           else 
              (if y:act B then 
-                 ((Takewhile (%a. a:int B)`schB)
-                     @@ (y>>(h`xs
-                              `schA
-                              `(TL`(Dropwhile (%a. a:int B)`schB))
+                 ((Takewhile (%a. a:int B)$schB)
+                     @@ (y>>(h$xs
+                              $schA
+                              $(TL$(Dropwhile (%a. a:int B)$schB))
                               )))
              else
                UU
@@ -56,8 +56,8 @@
        let trA = fst TracesA; sigA = snd TracesA; 
            trB = fst TracesB; sigB = snd TracesB       
        in
-       (    {tr. Filter (%a. a:actions sigA)`tr : trA}
-        Int {tr. Filter (%a. a:actions sigB)`tr : trB}
+       (    {tr. Filter (%a. a:actions sigA)$tr : trA}
+        Int {tr. Filter (%a. a:actions sigB)$tr : trB}
         Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
         asig_comp sigA sigB)"
 
@@ -65,7 +65,7 @@
 
 
 finiteR_mksch
-  "Finite (mksch A B`tr`x`y) --> Finite tr"
+  "Finite (mksch A B$tr$x$y) --> Finite tr"