--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Fri Oct 10 19:02:28 1997 +0200
@@ -45,7 +45,7 @@
Filter_ex2_def
- "Filter_ex2 sig == Filter (%x.fst x:actions sig)"
+ "Filter_ex2 sig == Filter (%x. fst x:actions sig)"
stutter_def
"stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
@@ -70,7 +70,7 @@
Int {ex. Filter_ex sigB (ProjB ex) : exB}
Int {ex. stutter sigA (ProjA ex)}
Int {ex. stutter sigB (ProjB ex)}
- Int {ex. Forall (%x.fst x:(actions sigA Un actions sigB)) (snd ex)},
+ Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
asig_comp sigA sigB)"
end
\ No newline at end of file