--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Fri Oct 10 19:02:28 1997 +0200
@@ -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)
+ ((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))
+ `(TL`(Dropwhile (%a. a:int A)`schA))
+ `(TL`(Dropwhile (%a. a:int B)`schB))
)))
else
- ((Takewhile (%a.a:int A)`schA)
+ ((Takewhile (%a. a:int A)`schA)
@@ (y>>(h`xs
- `(TL`(Dropwhile (%a.a:int A)`schA))
+ `(TL`(Dropwhile (%a. a:int A)`schA))
`schB)))
)
else
(if y:act B then
- ((Takewhile (%a.a:int B)`schB)
+ ((Takewhile (%a. a:int B)`schB)
@@ (y>>(h`xs
`schA
- `(TL`(Dropwhile (%a.a:int B)`schB))
+ `(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)"