--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Jul 17 12:43:32 1997 +0200
@@ -17,6 +17,8 @@
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
@@ -60,4 +62,14 @@
)
))))"
-end
\ No newline at end of file
+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)"
+
+end