src/HOLCF/IOA/meta_theory/CompoScheds.thy

--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Sep 02 15:54:47 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Sep 02 17:23:59 2005 +0200
@@ -1,59 +1,58 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
     ID:         $Id$
     Author:     Olaf Müller
+*)
 
-Compositionality on Schedule level.
-*) 
+header {* Compositionality on Schedule level *}
 
-CompoScheds = CompoExecs + 
-
-
+theory CompoScheds
+imports CompoExecs
+begin
 
 consts
 
  mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
-              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" 
- mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 
-              ('a,'s)pairs -> ('a,'t)pairs -> 
+              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution"
+ mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
+              ('a,'s)pairs -> ('a,'t)pairs ->
               ('s => 't => ('a,'s*'t)pairs)"
  par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"
 
 
-
 defs
 
-mkex_def  
-  "mkex A B sch exA exB == 
+mkex_def:
+  "mkex A B sch exA exB ==
        ((fst exA,fst exB),
         (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
 
-mkex2_def
-  "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of 
+mkex2_def:
+  "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of
        nil => nil
-    | x##xs => 
-      (case x of 
+    | x##xs =>
+      (case x of
         UU => UU
-      | Def y => 
-         (if y:act A then 
-             (if y:act B then 
+      | Def y =>
+         (if y:act A then
+             (if y:act B then
                 (case HD$exA of
                    UU => UU
                  | Def a => (case HD$exB of
                               UU => UU
-                            | Def b => 
+                            | Def b =>
                    (y,(snd a,snd b))>>
                      (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
               else
                 (case HD$exA of
                    UU => UU
-                 | Def a => 
+                 | Def a =>
                    (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
               )
-          else 
-             (if y:act B then 
+          else
+             (if y:act B then
                 (case HD$exB of
                    UU => UU
-                 | Def b => 
+                 | Def b =>
                    (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
              else
                UU
@@ -61,14 +60,16 @@
          )
        ))))"
 
-par_scheds_def
-  "par_scheds SchedsA SchedsB == 
-       let schA = fst SchedsA; sigA = snd SchedsA; 
-           schB = fst SchedsB; sigB = snd SchedsB       
+par_scheds_def:
+  "par_scheds SchedsA SchedsB ==
+       let schA = fst SchedsA; sigA = snd SchedsA;
+           schB = fst SchedsB; sigB = snd SchedsB
        in
        (    {sch. Filter (%a. a:actions sigA)$sch : schA}
         Int {sch. Filter (%a. a:actions sigB)$sch : schB}
         Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
         asig_comp sigA sigB)"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end