src/HOLCF/IOA/meta_theory/CompoTraces.thy

 CompoTraces = CompoScheds + ShortExecutions +
  
 
 consts  
 
- mksch     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
-
+ mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
+ par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
 
 defs
 
 mksch_def
   "mksch A B == (fix`(LAM h tr schA schB. case tr of 

              )
          )
        )))"
 
 
+par_traces_def
+  "par_traces TracesA TracesB == 
+       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}
+        Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
+        asig_comp sigA sigB)"
+
 rules
 
 
 finiteR_mksch
   "Finite (mksch A B`tr`x`y) --> Finite tr"
 
 
 
 end
-
-