--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Oct 13 10:22:28 1997 +0200
@@ -65,7 +65,7 @@
"!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
\ move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
-by (subgoal_tac "? ex.move A ex (f s) a (f t)" 1);
+by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
by (Asm_full_simp_tac 2);
by (etac exE 1);
by (rtac selectI 1);
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Mon Oct 13 10:22:28 1997 +0200
@@ -74,7 +74,7 @@
qed"sfilter_UU";
goal thy
-"!!x.x~=UU ==> sfilter`P`(x##xs)= \
+"!!x. x~=UU ==> sfilter`P`(x##xs)= \
\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
by (rtac trans 1);
by (stac sfilter_unfold 1);
@@ -102,7 +102,7 @@
qed"sforall2_UU";
goal thy
-"!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
+"!!x. x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
by (rtac trans 1);
by (stac sforall2_unfold 1);
by (Asm_full_simp_tac 1);
@@ -131,7 +131,7 @@
qed"stakewhile_UU";
goal thy
-"!!x.x~=UU ==> stakewhile`P`(x##xs) = \
+"!!x. x~=UU ==> stakewhile`P`(x##xs) = \
\ (If P`x then x##(stakewhile`P`xs) else nil fi)";
by (rtac trans 1);
by (stac stakewhile_unfold 1);
@@ -160,7 +160,7 @@
qed"sdropwhile_UU";
goal thy
-"!!x.x~=UU ==> sdropwhile`P`(x##xs) = \
+"!!x. x~=UU ==> sdropwhile`P`(x##xs) = \
\ (If P`x then sdropwhile`P`xs else x##xs fi)";
by (rtac trans 1);
by (stac sdropwhile_unfold 1);
@@ -191,7 +191,7 @@
qed"slast_UU";
goal thy
-"!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
+"!!x. x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
by (rtac trans 1);
by (stac slast_unfold 1);
by (Asm_full_simp_tac 1);
@@ -288,7 +288,7 @@
by (REPEAT (Asm_full_simp_tac 1));
qed"szip_UU2";
-goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
+goal thy "!!x. x~=UU ==> szip`(x##xs)`nil=UU";
by (rtac trans 1);
by (stac szip_unfold 1);
by (REPEAT (Asm_full_simp_tac 1));
@@ -417,7 +417,7 @@
by (fast_tac (HOL_cs addSDs seq.injects) 1);
qed"Finite_cons_a";
-goal thy "!!x.a~=UU ==>(Finite (a##x)) = (Finite x)";
+goal thy "!!x. a~=UU ==>(Finite (a##x)) = (Finite x)";
by (rtac iffI 1);
by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
by (REPEAT (assume_tac 1));
@@ -439,7 +439,7 @@
qed_goalw "seq_finite_ind_lemma" thy [seq.finite_def]
-"(!!n.P(seq_take n`s)) ==> seq_finite(s) -->P(s)"
+"(!!n. P(seq_take n`s)) ==> seq_finite(s) -->P(s)"
(fn prems =>
[
(strip_tac 1),
--- a/src/HOLCF/IOA/meta_theory/Seq.thy Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Mon Oct 13 10:22:28 1997 +0200
@@ -106,7 +106,7 @@
proj_def
- "nproj == (%n tr.HD`(iterate n TL tr))"
+ "nproj == (%n tr. HD`(iterate n TL tr))"
Partial_def
"Partial x == (seq_finite x) & ~(Finite x)"
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Oct 13 10:22:28 1997 +0200
@@ -95,7 +95,7 @@
goal thy "Filter P`s = Filter P`(Cut P s)";
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
,("Q1","%x.~ P x"), ("x1","s")]
(take_lemma_induct RS mp) 1);
by (Fast_tac 3);
@@ -112,7 +112,7 @@
goal thy "Cut P (Cut P s) = (Cut P s)";
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
,("Q1","%x.~ P x"), ("x1","s")]
(take_lemma_less_induct RS mp) 1);
by (Fast_tac 3);
@@ -130,7 +130,7 @@
goal thy "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
-by (res_inst_tac [("A1","%x.True")
+by (res_inst_tac [("A1","%x. True")
,("Q1","%x.~ P (f x)"), ("x1","s")]
(take_lemma_less_induct RS mp) 1);
by (Fast_tac 3);
@@ -230,17 +230,17 @@
goalw thy [schedules_def,has_schedule_def]
- "!! sch. [|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|] \
+ "!! sch. [|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
\ ==> ? sch. sch : schedules A & \
-\ tr = Filter (%a.a:ext A)`sch &\
+\ tr = Filter (%a. a:ext A)`sch &\
\ LastActExtsch A sch";
by (safe_tac set_cs);
-by (res_inst_tac [("x","filter_act`(Cut (%a.fst a:ext A) (snd ex))")] exI 1);
+by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
by (pair_tac "ex" 1);
by (safe_tac set_cs);
-by (res_inst_tac [("x","(x,Cut (%a.fst a:ext A) y)")] exI 1);
+by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1);
by (Asm_simp_tac 1);
(* Subgoal 1: Lemma: propagation of execution through Cut *)
@@ -250,14 +250,14 @@
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *)
by (simp_tac (!simpset addsimps [filter_act_def]) 1);
-by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
by (rtac (rewrite_rule [o_def] MapCut) 2);
by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
(* Subgoal 3: Lemma: Cut idempotent *)
by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
-by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
by (rtac (rewrite_rule [o_def] MapCut) 2);
by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
qed"exists_LastActExtsch";
@@ -268,7 +268,7 @@
(* ---------------------------------------------------------------- *)
goalw thy [LastActExtsch_def]
- "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
+ "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
\ ==> sch=nil";
by (dtac FilternPnilForallP 1);
by (etac conjE 1);
@@ -278,7 +278,7 @@
qed"LastActExtimplnil";
goalw thy [LastActExtsch_def]
- "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
+ "!! A. [| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
\ ==> sch=UU";
by (dtac FilternPUUForallP 1);
by (etac conjE 1);
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Mon Oct 13 10:14:52 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Mon Oct 13 10:22:28 1997 +0200
@@ -25,7 +25,7 @@
defs
LastActExtsch_def
- "LastActExtsch A sch == (Cut (%x.x: ext A) sch = sch)"
+ "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
LastActExtex_def
"LastActExtex A ex == LastActExtsch A (filter_act`ex)"