src/HOLCF/IOA/meta_theory/Traces.ML
changeset 3842 b55686a7b22c
parent 3521 bdc51b4c6050
child 4098 71e05eb27fb6
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -67,7 +67,7 @@
 goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \
 \      nil => TT \
 \    | x##xs => (flift1 \ 
-\            (%p.Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
+\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
 \             `x) \
 \   ))";
 by (rtac trans 1);
@@ -163,7 +163,7 @@
 
 goal thy 
   "!! A. is_trans_of A ==> \
-\ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
+\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
 
 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
 (* main case *)
@@ -174,7 +174,7 @@
 
 goal thy 
   "!! A.[|  is_trans_of A; x:executions A |] ==> \
-\ Forall (%a.a:act A) (filter_act`(snd x))";
+\ Forall (%a. a:act A) (filter_act`(snd x))";
 
 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
 by (pair_tac "x" 1);
@@ -184,7 +184,7 @@
 
 goalw thy [schedules_def,has_schedule_def]
   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
-\   Forall (%a.a:act A) x";
+\   Forall (%a. a:act A) x";
 
 by (fast_tac (!claset addSIs [exec_in_sig]) 1);
 qed"scheds_in_sig";
@@ -208,7 +208,7 @@
 
 (* second prefix notion for Finite x *)
 
-goal thy "! y s.is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
+goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
 by (pair_induct_tac "x" [is_exec_frag_def] 1);
 by (strip_tac 1);
 by (Seq_case_simp_tac "s" 1);