# HG changeset patch
# User paulson
# Date 899391235 -7200
# Node ID 8f4b72f0c15d9fc58333d355dbdf4fef6147219b
# Parent  2497807020fa0b84837c0e143a5e18d25bfc9989
Uncurried functions LeadsTo and reach
Deleted leading parameters thanks to new Goal command

diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Channel.ML
--- a/src/HOL/UNITY/Channel.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -14,7 +14,7 @@
 
 
 (*None represents "infinity" while Some represents proper integers*)
-Goalw [minSet_def] "!!A. minSet A = Some x --> x : A";
+Goalw [minSet_def] "minSet A = Some x --> x : A";
 by (Simp_tac 1);
 by (fast_tac (claset() addIs [LeastI]) 1);
 qed_spec_mp "minSet_eq_SomeD";
@@ -24,7 +24,7 @@
 qed_spec_mp "minSet_empty";
 Addsimps [minSet_empty];
 
-Goalw [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)";
+Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)";
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "minSet_nonempty";
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -14,9 +14,8 @@
 open Common;
 
 (*Misra's property CMT4: t exceeds no common meeting time*)
-Goal
-  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
-\           ==> stable Acts (atMost n)";
+Goal "[| ALL m. constrains Acts {m} (maxfg m); n: common |] \
+\     ==> stable Acts (atMost n)";
 by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
 by (asm_full_simp_tac
     (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
@@ -28,9 +27,8 @@
 			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
 qed "common_stable";
 
-Goal
-  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
-\           ==> reachable {0} Acts <= atMost n";
+Goal "[| ALL m. constrains Acts {m} (maxfg m); n: common |] \
+\     ==> reachable ({0},Acts) <= atMost n";
 by (rtac strongest_invariant 1);
 by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
 by (simp_tac (simpset() addsimps [atMost_def]) 1);
@@ -77,7 +75,7 @@
 Addsimps [atMost_Int_atLeast];
 
 Goal
-    "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
+    "[| ALL m. constrains Acts {m} (maxfg m); \
 \               ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \
 \               n: common;  id: Acts |]  \
 \            ==> leadsTo Acts (atMost n) common";
@@ -91,7 +89,7 @@
 
 (*The "ALL m: Compl common" form echoes CMT6.*)
 Goal
-    "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
+    "[| ALL m. constrains Acts {m} (maxfg m); \
 \               ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \
 \               n: common;  id: Acts |]  \
 \            ==> leadsTo Acts (atMost (LEAST n. n: common)) common";
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Deadlock.ML
--- a/src/HOL/UNITY/Deadlock.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -1,10 +1,15 @@
-
+(*  Title:      HOL/UNITY/Traces
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
 
-(*** Deadlock examples from section 5.6 ***)
+Deadlock examples from section 5.6 of 
+    Misra, "A Logic for Concurrent Programming", 1994
+*)
 
 (*Trivial, two-process case*)
 Goalw [constrains_def, stable_def]
-    "!!Acts. [| constrains Acts (A Int B) A;  constrains Acts (B Int A) B |] \
+    "[| constrains Acts (A Int B) A;  constrains Acts (B Int A) B |] \
 \           ==> stable Acts (A Int B)";
 by (Blast_tac 1);
 result();
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Mutex.thy
+(*  Title:      HOL/UNITY/Mutex
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -47,7 +47,7 @@
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 qed "stable_boolVars";
 
-Goal "reachable MInit mutex <= boolVars";
+Goal "reachable (MInit,mutex) <= boolVars";
 by (rtac strongest_invariant 1);
 by (rtac stable_boolVars 2);
 by (rewrite_goals_tac [MInit_def, boolVars_def]);
@@ -76,7 +76,7 @@
 qed "MInit_invar_1vn";
 
 (*The intersection is an invariant of the system*)
-Goal "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN";
+Goal "reachable (MInit,mutex) <= invariant 0 UU MM Int invariant 1 VV NN";
 by (simp_tac (simpset() addsimps
 	      [strongest_invariant, Int_greatest, stable_Int, 
 	       stable_invar_0um, stable_invar_1vn, 
@@ -94,7 +94,7 @@
 by Auto_tac;
 val lemma = result();
 
-Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable MInit mutex)";
+Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable (MInit,mutex))";
 by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
 qed "mutual_exclusion";
 
@@ -119,24 +119,24 @@
 by (constrains_tac 1);
 qed "U_F0";
 
-Goal "LeadsTo MInit mutex {s. s MM=1} {s. s PP = s VV & s MM = 2}";
+Goal "LeadsTo(MInit,mutex) {s. s MM=1} {s. s PP = s VV & s MM = 2}";
 by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
 by (ensures_tac "cmd1u" 1);
 qed "U_F1";
 
-Goal "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
+Goal "LeadsTo(MInit,mutex) {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
 by (cut_facts_tac [reachable_subset_invariant'] 1);
 by (ensures_tac "cmd2 0 MM" 1);
 qed "U_F2";
 
-Goalw [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}";
+Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s MM = 3} {s. s PP = 1}";
 by (rtac leadsTo_imp_LeadsTo 1); 
 by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
 by (ensures_tac "cmd4 1 MM" 2);
 by (ensures_tac "cmd3 UU MM" 1);
 qed "U_F3";
 
-Goal "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. s MM = 2} {s. s PP = 1}";
 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
@@ -144,13 +144,13 @@
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val lemma2 = result();
 
-Goal "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s PP = 1}";
 by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
 by (Blast_tac 1);
 val lemma1 = result();
 
 
-Goal "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
 	                addcongs [rev_conj_cong]) 1);
 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
@@ -159,7 +159,7 @@
 
 
 (*Misra's F4*)
-Goal "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. s UU = 1} {s. s PP = 1}";
 by (rtac LeadsTo_weaken_L 1);
 by (rtac lemma123 1);
 by (cut_facts_tac [reachable_subset_invariant'] 1);
@@ -174,24 +174,24 @@
 by (constrains_tac 1);
 qed "V_F0";
 
-Goal "LeadsTo MInit mutex {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
+Goal "LeadsTo(MInit,mutex) {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
 by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
 by (ensures_tac "cmd1v" 1);
 qed "V_F1";
 
-Goal "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
+Goal "LeadsTo(MInit,mutex) {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
 by (cut_facts_tac [reachable_subset_invariant'] 1);
 by (ensures_tac "cmd2 1 NN" 1);
 qed "V_F2";
 
-Goalw [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}";
+Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s NN = 3} {s. s PP = 0}";
 by (rtac leadsTo_imp_LeadsTo 1); 
 by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
 by (ensures_tac "cmd4 0 NN" 2);
 by (ensures_tac "cmd3 VV NN" 1);
 qed "V_F3";
 
-Goal "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. s NN = 2} {s. s PP = 0}";
 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
@@ -199,13 +199,13 @@
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val lemma2 = result();
 
-Goal "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s PP = 0}";
 by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
 by (Blast_tac 1);
 val lemma1 = result();
 
 
-Goal "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
 	                addcongs [rev_conj_cong]) 1);
 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
@@ -214,7 +214,7 @@
 
 
 (*Misra's F4*)
-Goal "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. s VV = 1} {s. s PP = 0}";
 by (rtac LeadsTo_weaken_L 1);
 by (rtac lemma123 1);
 by (cut_facts_tac [reachable_subset_invariant'] 1);
@@ -225,14 +225,14 @@
 (** Absence of starvation **)
 
 (*Misra's F6*)
-Goal "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}";
+Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s MM = 3}";
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac LeadsTo_cancel2 1);
 by (rtac U_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
 by (stac Un_commute 1);
 by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
 by (cut_facts_tac [reachable_subset_boolVars'] 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
@@ -240,7 +240,7 @@
 
 
 (*The same for V*)
-Goal "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}";
+Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s NN = 3}";
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac LeadsTo_cancel2 1);
 by (rtac V_F2 2);
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Network.thy
--- a/src/HOL/UNITY/Network.thy	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Network.thy	Thu Jul 02 16:53:55 1998 +0200
@@ -1,5 +1,17 @@
+(*  Title:      HOL/UNITY/Network
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Communication Network
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
+*)
+
 Network = UNITY +
 
+(*The state assigns a number to each process variable*)
+
 datatype pvar = Sent | Rcvd | Idle
 
 datatype pname = Aproc | Bproc
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -65,7 +65,7 @@
 by Auto_tac;
 qed "rinit_invariant";
 
-Goal "reachable rinit racts <= invariant";
+Goal "reachable (rinit,racts) <= invariant";
 by (simp_tac (simpset() addsimps
 	      [strongest_invariant, stable_invariant, rinit_invariant]) 1); 
 qed "reachable_subset_invariant";
@@ -134,13 +134,13 @@
 
 (*** Progress ***)
 
-Goalw [metric_def] "!!s. ~ s x ==> Suc (metric (s(x:=True))) = metric s";
+Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
 by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
 by Auto_tac;
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
 qed "Suc_metric";
 
-Goal "!!s. ~ s x ==> metric (s(x:=True)) < metric s";
+Goal "~ s x ==> metric (s(x:=True)) < metric s";
 by (etac (Suc_metric RS subst) 1);
 by (Blast_tac 1);
 qed "metric_less";
@@ -152,7 +152,7 @@
 	      simpset() addsimps [update_idem]));
 qed "metric_le";
 
-Goal "!!m. (u,v): edges ==> \
+Goal "(u,v): edges ==> \
 \              ensures racts ((metric-``{m}) Int {s. s u & ~ s v})  \
 \                            (metric-``(lessThan m))";
 by (ensures_tac "asgt u v" 1);
@@ -180,7 +180,7 @@
 by (rtac leadsTo_Un_fixedpoint 1);
 qed "leadsTo_fixedpoint";
 
-Goal "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }";
+Goal "LeadsTo(rinit,racts) UNIV { %v. (init, v) : edges^* }";
 by (stac (fixedpoint_invariant_correct RS sym) 1);
 by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1); 
 by (cut_facts_tac [reachable_subset_invariant] 1);
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -10,24 +10,24 @@
 
 open SubstAx;
 
-(*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B)
-                                           (reachable Init Acts Int B') *)
+(*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B)
+                                           (reachable(Init,Acts) Int B') *)
 bind_thm ("constrains_reachable",
 	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
 
 
 (*** Introduction rules: Basis, Trans, Union ***)
 
-Goalw [LeadsTo_def]
-    "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B";
+Goal "leadsTo Acts A B ==> LeadsTo(Init,Acts) A B";
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
 qed "leadsTo_imp_LeadsTo";
 
-Goalw [LeadsTo_def]
-    "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A'))   \
+Goal "[| constrains Acts (reachable(Init,Acts) Int (A - A'))   \
 \                               (A Un A'); \
-\               transient  Acts (reachable Init Acts Int (A-A')) |]   \
-\           ==> LeadsTo Init Acts A A'";
+\               transient  Acts (reachable(Init,Acts) Int (A-A')) |]   \
+\           ==> LeadsTo(Init,Acts) A A'";
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
 by (assume_tac 2);
 by (asm_simp_tac 
@@ -35,117 +35,117 @@
 			 stable_constrains_Int]) 1);
 qed "LeadsTo_Basis";
 
-Goalw [LeadsTo_def]
-    "!!Acts. [| LeadsTo Init Acts A B;  LeadsTo Init Acts B C |] \
-\            ==> LeadsTo Init Acts A C";
+Goal "[| LeadsTo(Init,Acts) A B;  LeadsTo(Init,Acts) B C |] \
+\            ==> LeadsTo(Init,Acts) A C";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
 qed "LeadsTo_Trans";
 
-val prems = goalw thy [LeadsTo_def]
- "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B";
+val [prem] = goalw thy [LeadsTo_def]
+ "(!!A. A : S ==> LeadsTo(Init,Acts) A B) ==> LeadsTo(Init,Acts) (Union S) B";
+by (Simp_tac 1);
 by (stac Int_Union 1);
-by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1);
+by (blast_tac (claset() addIs [leadsTo_UN,
+			        simplify (simpset()) prem]) 1);
 qed "LeadsTo_Union";
 
 
 (*** Derived rules ***)
 
-Goal "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV";
+Goal "id: Acts ==> LeadsTo(Init,Acts) A UNIV";
 by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
 				      Int_lower1 RS subset_imp_leadsTo]) 1);
 qed "LeadsTo_UNIV";
 Addsimps [LeadsTo_UNIV];
 
 (*Useful with cancellation, disjunction*)
-Goal "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'";
+Goal "LeadsTo(Init,Acts) A (A' Un A') ==> LeadsTo(Init,Acts) A A'";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "LeadsTo_Un_duplicate";
 
-Goal "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)";
+Goal "LeadsTo(Init,Acts) A (A' Un C Un C) ==> LeadsTo(Init,Acts) A (A' Un C)";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "LeadsTo_Un_duplicate2";
 
 val prems = goal thy
-   "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \
-\   ==> LeadsTo Init Acts (UN i:I. A i) B";
+   "(!!i. i : I ==> LeadsTo(Init,Acts) (A i) B) \
+\   ==> LeadsTo(Init,Acts) (UN i:I. A i) B";
 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
 qed "LeadsTo_UN";
 
 (*Binary union introduction rule*)
 Goal
-  "!!C. [| LeadsTo Init Acts A C; LeadsTo Init Acts B C |] ==> LeadsTo Init Acts (A Un B) C";
+  "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
 by (stac Un_eq_Union 1);
 by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
 qed "LeadsTo_Un";
 
 
-Goalw [LeadsTo_def]
-    "!!A B. [| reachable Init Acts Int A <= B;  id: Acts |] \
-\           ==> LeadsTo Init Acts A B";
+Goal "[| reachable(Init,Acts) Int A <= B;  id: Acts |] \
+\            ==> LeadsTo(Init,Acts) A B";
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "Int_subset_imp_LeadsTo";
 
-Goalw [LeadsTo_def]
-    "!!A B. [| A <= B;  id: Acts |] \
-\           ==> LeadsTo Init Acts A B";
+Goal "[| A <= B;  id: Acts |] ==> LeadsTo(Init,Acts) A B";
+by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "subset_imp_LeadsTo";
 
 bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
 Addsimps [empty_LeadsTo];
 
-Goal
-    "!!A B. [| reachable Init Acts Int A = {};  id: Acts |] \
-\           ==> LeadsTo Init Acts A B";
+Goal "[| reachable(Init,Acts) Int A = {};  id: Acts |] \
+\            ==> LeadsTo(Init,Acts) A B";
 by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
 qed "Int_empty_LeadsTo";
 
 
-Goalw [LeadsTo_def]
-    "!!Acts. [| LeadsTo Init Acts A A';   \
-\               reachable Init Acts Int A' <= B' |] \
-\            ==> LeadsTo Init Acts A B'";
+Goal "[| LeadsTo(Init,Acts) A A';   \
+\                reachable(Init,Acts) Int A' <= B' |] \
+\             ==> LeadsTo(Init,Acts) A B'";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
 qed_spec_mp "LeadsTo_weaken_R";
 
 
-Goalw [LeadsTo_def]
-    "!!Acts. [| LeadsTo Init Acts A A'; \
-     \               reachable Init Acts Int B <= A; id: Acts |]  \
-\            ==> LeadsTo Init Acts B A'";
+Goal "[| LeadsTo(Init,Acts) A A'; \
+\                reachable(Init,Acts) Int B <= A; id: Acts |]  \
+\             ==> LeadsTo(Init,Acts) B A'";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
 qed_spec_mp "LeadsTo_weaken_L";
 
 
 (*Distributes over binary unions*)
 Goal
-  "!!C. id: Acts ==> \
-\       LeadsTo Init Acts (A Un B) C  =  \
-\       (LeadsTo Init Acts A C & LeadsTo Init Acts B C)";
+  "id: Acts ==> \
+\       LeadsTo(Init,Acts) (A Un B) C  =  \
+\       (LeadsTo(Init,Acts) A C & LeadsTo(Init,Acts) B C)";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Un_distrib";
 
 Goal
-  "!!C. id: Acts ==> \
-\       LeadsTo Init Acts (UN i:I. A i) B  =  \
-\       (ALL i : I. LeadsTo Init Acts (A i) B)";
+  "id: Acts ==> \
+\       LeadsTo(Init,Acts) (UN i:I. A i) B  =  \
+\       (ALL i : I. LeadsTo(Init,Acts) (A i) B)";
 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_UN_distrib";
 
 Goal
-  "!!C. id: Acts ==> \
-\       LeadsTo Init Acts (Union S) B  =  \
-\       (ALL A : S. LeadsTo Init Acts A B)";
+  "id: Acts ==> \
+\       LeadsTo(Init,Acts) (Union S) B  =  \
+\       (ALL A : S. LeadsTo(Init,Acts) A B)";
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Union_distrib";
 
 
 Goal 
-   "!!Acts. [| LeadsTo Init Acts A A'; id: Acts;   \
-\               reachable Init Acts Int B  <= A;     \
-\               reachable Init Acts Int A' <= B' |] \
-\           ==> LeadsTo Init Acts B B'";
+   "[| LeadsTo(Init,Acts) A A'; id: Acts;   \
+\               reachable(Init,Acts) Int B  <= A;     \
+\               reachable(Init,Acts) Int A' <= B' |] \
+\           ==> LeadsTo(Init,Acts) B B'";
 (*PROOF FAILED: why?*)
 by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
 			       LeadsTo_weaken_L]) 1);
@@ -154,8 +154,8 @@
 
 (*Set difference: maybe combine with leadsTo_weaken_L??*)
 Goal
-  "!!C. [| LeadsTo Init Acts (A-B) C; LeadsTo Init Acts B C; id: Acts |] \
-\       ==> LeadsTo Init Acts A C";
+  "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
+\       ==> LeadsTo(Init,Acts) A C";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
 qed "LeadsTo_Diff";
 
@@ -164,8 +164,8 @@
     see ball_constrains_UN in UNITY.ML***)
 
 val prems = goal thy
-   "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \
-\   ==> LeadsTo Init Acts (UN i:I. A i) (UN i:I. A' i)";
+   "(!! i. i:I ==> LeadsTo(Init,Acts) (A i) (A' i)) \
+\   ==> LeadsTo(Init,Acts) (UN i:I. A i) (UN i:I. A' i)";
 by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R] 
                         addIs prems) 1);
@@ -174,23 +174,23 @@
 
 (*Version with no index set*)
 val prems = goal thy
-   "(!! i. LeadsTo Init Acts (A i) (A' i)) \
-\   ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
+   "(!! i. LeadsTo(Init,Acts) (A i) (A' i)) \
+\   ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [LeadsTo_UN_UN] 
                         addIs prems) 1);
 qed "LeadsTo_UN_UN_noindex";
 
 (*Version with no index set*)
 Goal
-   "!!Acts. ALL i. LeadsTo Init Acts (A i) (A' i) \
-\           ==> LeadsTo Init Acts (UN i. A i) (UN i. A' i)";
+   "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
+\           ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
 qed "all_LeadsTo_UN_UN";
 
 
 (*Binary union version*)
-Goal "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \
-\                 ==> LeadsTo Init Acts (A Un B) (A' Un B')";
+Goal "[| LeadsTo(Init,Acts) A A'; LeadsTo(Init,Acts) B B' |] \
+\                 ==> LeadsTo(Init,Acts) (A Un B) (A' Un B')";
 by (blast_tac (claset() addIs [LeadsTo_Un, 
 			       LeadsTo_weaken_R]) 1);
 qed "LeadsTo_Un_Un";
@@ -199,31 +199,31 @@
 (** The cancellation law **)
 
 Goal
-   "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts B B'; \
+   "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
 \              id: Acts |]    \
-\           ==> LeadsTo Init Acts A (A' Un B')";
+\           ==> LeadsTo(Init,Acts) A (A' Un B')";
 by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
 			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
 qed "LeadsTo_cancel2";
 
 Goal
-   "!!Acts. [| LeadsTo Init Acts A (A' Un B); LeadsTo Init Acts (B-A') B'; id: Acts |] \
-\           ==> LeadsTo Init Acts A (A' Un B')";
+   "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
+\           ==> LeadsTo(Init,Acts) A (A' Un B')";
 by (rtac LeadsTo_cancel2 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
 qed "LeadsTo_cancel_Diff2";
 
 Goal
-   "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts B B'; id: Acts |] \
-\           ==> LeadsTo Init Acts A (B' Un A')";
+   "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
+\           ==> LeadsTo(Init,Acts) A (B' Un A')";
 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
 by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
 qed "LeadsTo_cancel1";
 
 Goal
-   "!!Acts. [| LeadsTo Init Acts A (B Un A'); LeadsTo Init Acts (B-A') B'; id: Acts |] \
-\           ==> LeadsTo Init Acts A (B' Un A')";
+   "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
+\           ==> LeadsTo(Init,Acts) A (B' Un A')";
 by (rtac LeadsTo_cancel1 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
@@ -233,9 +233,8 @@
 
 (** The impossibility law **)
 
-Goalw [LeadsTo_def]
-    "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A  = {}";
-by (Full_simp_tac 1);
+Goal "LeadsTo(Init,Acts) A {} ==> reachable(Init,Acts) Int A  = {}";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (etac leadsTo_empty 1);
 qed "LeadsTo_empty";
 
@@ -243,22 +242,21 @@
 (** PSP: Progress-Safety-Progress **)
 
 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
-Goalw [LeadsTo_def]
-   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
-\           ==> LeadsTo Init Acts (A Int B) (A' Int B)";
-by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1);
+Goal "[| LeadsTo(Init,Acts) A A'; stable Acts B |] \
+\           ==> LeadsTo(Init,Acts) (A Int B) (A' Int B)";
+by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, 
+					   PSP_stable]) 1);
 qed "R_PSP_stable";
 
-Goal
-   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
-\           ==> LeadsTo Init Acts (B Int A) (B Int A')";
+Goal "[| LeadsTo(Init,Acts) A A'; stable Acts B |] \
+\             ==> LeadsTo(Init,Acts) (B Int A) (B Int A')";
 by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
 qed "R_PSP_stable2";
 
 
-Goalw [LeadsTo_def]
-   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
-\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))";
+Goal "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
+\           ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B) Un (B' - B))";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (dtac PSP 1);
 by (etac constrains_reachable 1);
 by (etac leadsTo_weaken 2);
@@ -266,14 +264,14 @@
 qed "R_PSP";
 
 Goal
-   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
-\           ==> LeadsTo Init Acts (B Int A) ((B Int A') Un (B' - B))";
+   "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
+\           ==> LeadsTo(Init,Acts) (B Int A) ((B Int A') Un (B' - B))";
 by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
 qed "R_PSP2";
 
 Goalw [unless_def]
-   "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \
-\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')";
+   "[| LeadsTo(Init,Acts) A A'; unless Acts B B'; id: Acts |] \
+\           ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B) Un B')";
 by (dtac R_PSP 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
@@ -287,12 +285,13 @@
 (*** Induction rules ***)
 
 (** Meta or object quantifier ????? **)
-Goalw [LeadsTo_def]
-   "!!Acts. [| wf r;     \
-\              ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
+Goal
+   "[| wf r;     \
+\              ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
 \                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \              id: Acts |] \
-\           ==> LeadsTo Init Acts A B";
+\           ==> LeadsTo(Init,Acts) A B";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (etac leadsTo_wf_induct 1);
 by (assume_tac 2);
 by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
@@ -300,11 +299,11 @@
 
 
 Goal
-   "!!Acts. [| wf r;     \
-\              ALL m:I. LeadsTo Init Acts (A Int f-``{m})                   \
+   "[| wf r;     \
+\              ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m})                   \
 \                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \              id: Acts |] \
-\           ==> LeadsTo Init Acts A ((A - (f-``I)) Un B)";
+\           ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
 by (etac LeadsTo_wf_induct 1);
 by Safe_tac;
 by (case_tac "m:I" 1);
@@ -314,20 +313,20 @@
 
 
 Goal
-   "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
+   "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
 \                                  ((A Int f-``(lessThan m)) Un B);   \
 \              id: Acts |] \
-\           ==> LeadsTo Init Acts A B";
+\           ==> LeadsTo(Init,Acts) A B";
 by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
 by (assume_tac 2);
 by (Asm_simp_tac 1);
 qed "R_lessThan_induct";
 
 Goal
-   "!!Acts. [| ALL m:(greaterThan l). LeadsTo Init Acts (A Int f-``{m})   \
+   "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
 \                                        ((A Int f-``(lessThan m)) Un B);   \
 \              id: Acts |] \
-\           ==> LeadsTo Init Acts A ((A Int (f-``(atMost l))) Un B)";
+\           ==> LeadsTo(Init,Acts) A ((A Int (f-``(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
 by (rtac (wf_less_than RS R_bounded_induct) 1);
 by (assume_tac 2);
@@ -335,10 +334,10 @@
 qed "R_lessThan_bounded_induct";
 
 Goal
-   "!!Acts. [| ALL m:(lessThan l). LeadsTo Init Acts (A Int f-``{m})   \
+   "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
 \                                    ((A Int f-``(greaterThan m)) Un B);   \
 \              id: Acts |] \
-\           ==> LeadsTo Init Acts A ((A Int (f-``(atLeast l))) Un B)";
+\           ==> LeadsTo(Init,Acts) A ((A Int (f-``(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
     (wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
 by (assume_tac 2);
@@ -353,20 +352,20 @@
 
 (*** Completion: Binary and General Finite versions ***)
 
-Goalw [LeadsTo_def]
-   "!!Acts. [| LeadsTo Init Acts A A';  stable Acts A';   \
-\              LeadsTo Init Acts B B';  stable Acts B';  id: Acts |] \
-\           ==> LeadsTo Init Acts (A Int B) (A' Int B')";
+Goal
+   "[| LeadsTo(Init,Acts) A A';  stable Acts A';   \
+\              LeadsTo(Init,Acts) B B';  stable Acts B';  id: Acts |] \
+\           ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
                         addSIs [stable_Int, stable_reachable]) 1);
 qed "R_stable_completion";
 
 
-Goal
-   "!!Acts. [| finite I;  id: Acts |]                     \
-\           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i)) -->  \
+Goal "[| finite I;  id: Acts |]                     \
+\           ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) -->  \
 \               (ALL i:I. stable Acts (A' i)) -->         \
-\               LeadsTo Init Acts (INT i:I. A i) (INT i:I. A' i)";
+\               LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
 by (etac finite_induct 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac 
@@ -375,13 +374,13 @@
 qed_spec_mp "R_finite_stable_completion";
 
 
-Goalw [LeadsTo_def]
- "!!Acts. [| LeadsTo Init Acts A (A' Un C);  constrains Acts A' (A' Un C); \
-\            LeadsTo Init Acts B (B' Un C);  constrains Acts B' (B' Un C); \
+Goal
+ "[| LeadsTo(Init,Acts) A (A' Un C);  constrains Acts A' (A' Un C); \
+\            LeadsTo(Init,Acts) B (B' Un C);  constrains Acts B' (B' Un C); \
 \            id: Acts |] \
-\         ==> LeadsTo Init Acts (A Int B) ((A' Int B') Un C)";
+\         ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
 
-by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
 by (dtac completion 1);
 by (assume_tac 2);
 by (ALLGOALS 
@@ -392,10 +391,10 @@
 
 
 Goal
-   "!!Acts. [| finite I;  id: Acts |] \
-\           ==> (ALL i:I. LeadsTo Init Acts (A i) (A' i Un C)) -->  \
+   "[| finite I;  id: Acts |] \
+\           ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) -->  \
 \               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
-\               LeadsTo Init Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
+\               LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 02 16:53:55 1998 +0200
@@ -10,10 +10,10 @@
 
 constdefs
 
-   LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool"
-    "LeadsTo Init Acts A B ==
-     leadsTo Acts (reachable Init Acts Int A)
-                  (reachable Init Acts Int B)"
+   LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool"
+    "LeadsTo == %(Init,Acts) A B.
+		 leadsTo Acts (reachable (Init,Acts) Int A)
+			      (reachable (Init,Acts) Int B)"
 
 
 end
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Token.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -16,11 +16,11 @@
 
 AddIffs [N_positive, skip];
 
-Goalw [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
+Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j";
 by Auto_tac;
 qed "HasToK_partition";
 
-Goalw Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+Goalw Token_defs "s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
 by (Simp_tac 1);
 by (exhaust_tac "s (Suc i)" 1);
 by Auto_tac;
@@ -61,13 +61,13 @@
 by (Blast_tac 1);
 qed"wf_nodeOrder";
 
-Goal "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
+Goal "[| m<n; Suc m ~= n |] ==> Suc(m) < n";
     by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
     by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
     qed "Suc_lessI";
 
 Goalw [nodeOrder_def, next_def, inv_image_def]
-    "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
+    "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
 by (auto_tac (claset(),
 	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
 by (dtac sym 1);
@@ -100,7 +100,7 @@
 (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
 Goal
- "!!i. [| i<N; j<N |] ==> \
+ "[| i<N; j<N |] ==> \
 \      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
 by (case_tac "i=j" 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
@@ -112,7 +112,7 @@
 
 (*Chapter 4 variant, the one actually used below.*)
 Goal
- "!!i. [| i<N; j<N; i~=j |] ==> \
+ "[| i<N; j<N; i~=j |] ==> \
 \      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
 by (rtac (TR7 RS leadsTo_weaken_R) 1);
 by (Clarify_tac 1);
@@ -127,7 +127,7 @@
 
 (*Misra's TR9: the token reaches an arbitrary node*)
 Goal
- "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
+ "j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
 by (rtac leadsTo_weaken_R 1);
 by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
      (wf_nodeOrder RS bounded_induct) 1);
@@ -141,7 +141,7 @@
 qed "leadsTo_j";
 
 (*Misra's TR8: a hungry process eventually eats*)
-Goal "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
+Goal "j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
 by (rtac TR6 2);
 by (rtac leadsTo_weaken_R 1);
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -1,39 +1,81 @@
+(*  Title:      HOL/UNITY/Traces
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Definitions of
+  * traces: the possible execution traces
+  * reachable: the set of reachable states
+
+*)
+
 open Traces;
 
-Goal "reachable Init Acts <= {s. EX evs. s#evs: traces Init Acts}";
-by (rtac subsetI 1);
-be reachable.induct 1;
-by (REPEAT (blast_tac (claset() addIs traces.intrs) 1));
-val lemma1 = result();
+
+(****
+Now simulate the inductive definition (illegal due to paired arguments)
+
+inductive "reachable(Init,Acts)"
+  intrs 
+    Init  "s: Init ==> s : reachable(Init,Acts)"
+
+    Acts  "[| act: Acts;  s : reachable(Init,Acts);  (s,s'): act |]
+	   ==> s' : reachable(Init,Acts)"
 
-Goal "!!evs. evs : traces Init Acts \
-\                ==> ALL s evs'. evs = s#evs' --> s: reachable Init Acts";
-be traces.induct 1;
-by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-val lemma2 = normalize_thm [RSmp, RSspec] (result());
+This amounts to an equivalence proof for the definition actually used, 
+****)
+
 
-Goal "{s. EX evs. s#evs: traces Init Acts} <= reachable Init Acts";
-by (blast_tac (claset() addIs [lemma2]) 1);
-val lemma3 = result();
+(** reachable: Deriving the Introduction rules **)
 
-Goal "reachable Init Acts = {s. EX evs. s#evs: traces Init Acts}";
-by (rtac ([lemma1,lemma3] MRS equalityI) 1);
-qed "reachable_eq_traces";
+Goal "s: Init ==> s : reachable(Init,Acts)";
+by (simp_tac (simpset() addsimps [reachable_def]) 1);
+by (blast_tac (claset() addIs traces.intrs) 1);
+qed "reachable_Init";
 
 
-(*Could/should this be proved?*)
-Goal "reachable Init Acts = (UN evs: traces Init Acts. set evs)";
+Goal "[| act: Acts;  s : reachable(Init,Acts) |] \
+\     ==> (s,s'): act --> s' : reachable(Init,Acts)";
+by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
+by (etac exE 1);
+be traces.induct 1;
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (claset() addIs traces.intrs)));
+qed_spec_mp "reachable_Acts";
+
+
+val major::prems = 
+Goalw [reachable_def] 
+  "[| za : reachable(Init,Acts);  \
+\     !!s. s : Init ==> P s;      \
+\     !!act s s'.  \
+\        [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |]  \
+\        ==> P s' |] \
+\  ==> P za";
+by (cut_facts_tac [major] 1);
+auto();
+be traces.induct 1;
+by (ALLGOALS (blast_tac (claset() addIs prems)));
+qed "reachable_induct";
+
+structure reachable = 
+  struct 
+  val Init = reachable_Init
+  val Acts = reachable_Acts
+  val intrs = [reachable_Init, reachable_Acts]
+  val induct = reachable_induct
+  end;
 
 
 (*The strongest invariant is the set of all reachable states!*)
 Goalw [stable_def, constrains_def]
-    "!!A. [| Init<=A;  stable Acts A |] ==> reachable Init Acts <= A";
+    "[| Init<=A;  stable Acts A |] ==> reachable(Init,Acts) <= A";
 by (rtac subsetI 1);
 be reachable.induct 1;
 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
 qed "strongest_invariant";
 
-Goal "stable Acts (reachable Init Acts)";
+Goal "stable Acts (reachable(Init,Acts))";
 by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI]
 				addIs reachable.intrs) 1));
 qed "stable_reachable";
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/Traces.thy
--- a/src/HOL/UNITY/Traces.thy	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy	Thu Jul 02 16:53:55 1998 +0200
@@ -1,23 +1,30 @@
+(*  Title:      HOL/UNITY/Traces
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Inductive definitions of
+  * traces: the possible execution traces
+  * reachable: the set of reachable states
+*)
+
 Traces = UNITY +
 
-consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
+consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
 
-inductive "traces Init Acts"
+  (*Initial states and program => (final state, reversed trace to it)...
+    Arguments MUST be curried in an inductive definition*)
+
+inductive "traces Init Acts"  
   intrs 
          (*Initial trace is empty*)
-    Init  "s: Init ==> [s] : traces Init Acts"
+    Init  "s: Init ==> (s,[]) : traces Init Acts"
 
-    Acts  "[| act: Acts;  s#evs : traces Init Acts;  (s,s'): act |]
-	   ==> s'#s#evs : traces Init Acts"
+    Acts  "[| act: Acts;  (s,evs) : traces Init Acts;  (s,s'): act |]
+	   ==> (s', s#evs) : traces Init Acts"
 
 
-consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
-
-inductive "reachable Init Acts"
-  intrs 
-    Init  "s: Init ==> s : reachable Init Acts"
-
-    Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
-	   ==> s' : reachable Init Acts"
+constdefs reachable :: "'a set * ('a * 'a)set set => 'a set"
+  "reachable == %(Init,Acts). {s. EX evs. (s,evs): traces Init Acts}"
 
 end
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -18,11 +18,11 @@
     be any set including A Int C and contained in A Un C, such as B=A or B=C.
 **)
 
-Goal "!!x. [| A Int C <= B; B <= A Un C |] \
+Goal "[| A Int C <= B; B <= A Un C |] \
 \              ==> (A Int B) Un (Compl A Int C) = B Un C";
 by (Blast_tac 1);
 
-Goal "!!x. [| A Int C <= B; B <= A Un C |] \
+Goal "[| A Int C <= B; B <= A Un C |] \
 \              ==> (A Un B) Int (Compl A Un C) = B Int C";
 by (Blast_tac 1);
 
@@ -64,7 +64,7 @@
 qed "constrainsI";
 
 Goalw [constrains_def]
-    "!!Acts. [| constrains Acts A A'; act: Acts;  (s,s'): act;  s: A |] \
+    "[| constrains Acts A A'; act: Acts;  (s,s'): act;  s: A |] \
 \            ==> s': A'";
 by (Blast_tac 1);
 qed "constrainsD";
@@ -79,23 +79,23 @@
 AddIffs [constrains_empty, constrains_UNIV];
 
 Goalw [constrains_def]
-    "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
+    "[| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
 by (Blast_tac 1);
 qed "constrains_weaken_R";
 
 Goalw [constrains_def]
-    "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
+    "[| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
 by (Blast_tac 1);
 qed "constrains_weaken_L";
 
 Goalw [constrains_def]
-   "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
+   "[| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
 by (Blast_tac 1);
 qed "constrains_weaken";
 
 (*Set difference: UNUSED*)
 Goalw [constrains_def]
-  "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \
+  "[| constrains Acts (A-B) C; constrains Acts B C |] \
 \       ==> constrains Acts A C";
 by (Blast_tac 1);
 qed "constrains_Diff";
@@ -103,19 +103,19 @@
 (** Union **)
 
 Goalw [constrains_def]
-    "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
+    "[| constrains Acts A A'; constrains Acts B B' |]   \
 \           ==> constrains Acts (A Un B) (A' Un B')";
 by (Blast_tac 1);
 qed "constrains_Un";
 
 Goalw [constrains_def]
-    "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
+    "ALL i:I. constrains Acts (A i) (A' i) \
 \    ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)";
 by (Blast_tac 1);
 qed "ball_constrains_UN";
 
 Goalw [constrains_def]
-    "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
+    "[| ALL i. constrains Acts (A i) (A' i) |] \
 \           ==> constrains Acts (UN i. A i) (UN i. A' i)";
 by (Blast_tac 1);
 qed "all_constrains_UN";
@@ -123,31 +123,31 @@
 (** Intersection **)
 
 Goalw [constrains_def]
-    "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
+    "[| constrains Acts A A'; constrains Acts B B' |]   \
 \           ==> constrains Acts (A Int B) (A' Int B')";
 by (Blast_tac 1);
 qed "constrains_Int";
 
 Goalw [constrains_def]
-    "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
+    "ALL i:I. constrains Acts (A i) (A' i) \
 \    ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)";
 by (Blast_tac 1);
 qed "ball_constrains_INT";
 
 Goalw [constrains_def]
-    "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
+    "[| ALL i. constrains Acts (A i) (A' i) |] \
 \           ==> constrains Acts (INT i. A i) (INT i. A' i)";
 by (Blast_tac 1);
 qed "all_constrains_INT";
 
 Goalw [stable_def, constrains_def]
-    "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |]   \
+    "[| stable Acts C; constrains Acts A (C Un A') |]   \
 \           ==> constrains Acts (C Un A) (C Un A')";
 by (Blast_tac 1);
 qed "stable_constrains_Un";
 
 Goalw [stable_def, constrains_def]
-    "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |]   \
+    "[| stable Acts C; constrains Acts (C Int A) A' |]   \
 \           ==> constrains Acts (C Int A) (C Int A')";
 by (Blast_tac 1);
 qed "stable_constrains_Int";
@@ -156,35 +156,35 @@
 (*** stable ***)
 
 Goalw [stable_def]
-    "!!Acts. constrains Acts A A ==> stable Acts A";
+    "constrains Acts A A ==> stable Acts A";
 by (assume_tac 1);
 qed "stableI";
 
 Goalw [stable_def]
-    "!!Acts. stable Acts A ==> constrains Acts A A";
+    "stable Acts A ==> constrains Acts A A";
 by (assume_tac 1);
 qed "stableD";
 
 Goalw [stable_def]
-    "!!Acts. [| stable Acts A; stable Acts A' |]   \
+    "[| stable Acts A; stable Acts A' |]   \
 \           ==> stable Acts (A Un A')";
 by (blast_tac (claset() addIs [constrains_Un]) 1);
 qed "stable_Un";
 
 Goalw [stable_def]
-    "!!Acts. [| stable Acts A; stable Acts A' |]   \
+    "[| stable Acts A; stable Acts A' |]   \
 \           ==> stable Acts (A Int A')";
 by (blast_tac (claset() addIs [constrains_Int]) 1);
 qed "stable_Int";
 
 Goalw [constrains_def]
-    "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'";
+    "[| constrains Acts A A'; id: Acts |] ==> A<=A'";
 by (Blast_tac 1);
 qed "constrains_imp_subset";
 
 
 Goalw [constrains_def]
-    "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |]   \
+    "[| id: Acts; constrains Acts A B; constrains Acts B C |]   \
 \           ==> constrains Acts A C";
 by (Blast_tac 1);
 qed "constrains_trans";
@@ -194,7 +194,7 @@
   Should the premise be !!m instead of ALL m ?  Would make it harder to use
   in forward proof.*)
 Goalw [constrains_def]
-    "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \
+    "[| ALL m. constrains Acts {s. s x = m} (B m) |] \
 \           ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
 by (Blast_tac 1);
 qed "elimination";
@@ -202,14 +202,14 @@
 (*As above, but for the trivial case of a one-variable state, in which the
   state is identified with its one variable.*)
 Goalw [constrains_def]
-    "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \
+    "[| ALL m. constrains Acts {m} (B m) |] \
 \           ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)";
 by (Blast_tac 1);
 qed "elimination_sing";
 
 
 Goalw [constrains_def]
-   "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
+   "[| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
 \           ==> constrains Acts A (A' Un B')";
 by (Blast_tac 1);
 qed "constrains_cancel";
@@ -224,6 +224,6 @@
 qed "constrains_strongest_rhs";
 
 Goalw [constrains_def, strongest_rhs_def]
-    "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B";
+    "constrains Acts A B ==> strongest_rhs Acts A <= B";
 by (Blast_tac 1);
 qed "strongest_rhs_is_strongest";
diff -r 2497807020fa -r 8f4b72f0c15d src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Thu Jul 02 16:53:55 1998 +0200
@@ -18,19 +18,19 @@
 (*** transient ***)
 
 Goalw [stable_def, constrains_def, transient_def]
-    "!!A. [| stable Acts A; transient Acts A |] ==> A = {}";
+    "[| stable Acts A; transient Acts A |] ==> A = {}";
 by (Blast_tac 1);
 qed "stable_transient_empty";
 
 Goalw [transient_def]
-    "!!A. [| transient Acts A; B<=A |] ==> transient Acts B";
+    "[| transient Acts A; B<=A |] ==> transient Acts B";
 by (Clarify_tac 1);
 by (rtac bexI 1 THEN assume_tac 2);
 by (Blast_tac 1);
 qed "transient_strengthen";
 
 Goalw [transient_def]
-    "!!A. [| act:Acts;  A <= Domain act;  act^^A <= Compl A |] \
+    "[| act:Acts;  A <= Domain act;  act^^A <= Compl A |] \
 \         ==> transient Acts A";
 by (Blast_tac 1);
 qed "transient_mem";
@@ -39,31 +39,31 @@
 (*** ensures ***)
 
 Goalw [ensures_def]
-    "!!Acts. [| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
+    "[| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
 \            ==> ensures Acts A B";
 by (Blast_tac 1);
 qed "ensuresI";
 
 Goalw [ensures_def]
-    "!!Acts. ensures Acts A B  \
+    "ensures Acts A B  \
 \            ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
 by (Blast_tac 1);
 qed "ensuresD";
 
 (*The L-version (precondition strengthening) doesn't hold for ENSURES*)
 Goalw [ensures_def]
-    "!!Acts. [| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'";
+    "[| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'";
 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
 qed "ensures_weaken_R";
 
 Goalw [ensures_def, constrains_def, transient_def]
-    "!!Acts. Acts ~= {} ==> ensures Acts A UNIV";
+    "Acts ~= {} ==> ensures Acts A UNIV";
 by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
 by (Blast_tac 1);
 qed "ensures_UNIV";
 
 Goalw [ensures_def]
-    "!!Acts. [| stable Acts C; \
+    "[| stable Acts C; \
 \               constrains Acts (C Int (A - A')) (A Un A'); \
 \               transient  Acts (C Int (A-A')) |]   \
 \           ==> ensures Acts (C Int A) (C Int A')";
@@ -79,17 +79,17 @@
 bind_thm ("leadsTo_Basis", leadsto.Basis);
 bind_thm ("leadsTo_Trans", leadsto.Trans);
 
-Goal "!!Acts. act: Acts ==> leadsTo Acts A UNIV";
+Goal "act: Acts ==> leadsTo Acts A UNIV";
 by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
 qed "leadsTo_UNIV";
 Addsimps [leadsTo_UNIV];
 
 (*Useful with cancellation, disjunction*)
-Goal "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
+Goal "leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "leadsTo_Un_duplicate";
 
-Goal "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";
+Goal "leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
 qed "leadsTo_Un_duplicate2";
 
@@ -107,7 +107,7 @@
 
 (*Binary union introduction rule*)
 Goal
-  "!!C. [| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C";
+  "[| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C";
 by (stac Un_eq_Union 1);
 by (blast_tac (claset() addIs [leadsTo_Union]) 1);
 qed "leadsTo_Un";
@@ -126,7 +126,7 @@
 qed "leadsTo_induct";
 
 
-Goal "!!A B. [| A<=B;  id: Acts |] ==> leadsTo Acts A B";
+Goal "[| A<=B;  id: Acts |] ==> leadsTo Acts A B";
 by (rtac leadsTo_Basis 1);
 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
 by (Blast_tac 1);
@@ -138,7 +138,7 @@
 
 (*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
   needs the extra premise id:Acts*)
-Goal "!!Acts. leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'";
+Goal "leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'";
 by (etac leadsTo_induct 1);
 by (Clarify_tac 3);
 by (blast_tac (claset() addIs [leadsTo_Union]) 3);
@@ -147,7 +147,7 @@
 qed_spec_mp "leadsTo_weaken_R";
 
 
-Goal "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
+Goal "[| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
 \                 leadsTo Acts B A'";
 by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
 			       subset_imp_leadsTo]) 1);
@@ -155,26 +155,26 @@
 
 (*Distributes over binary unions*)
 Goal
-  "!!C. id: Acts ==> \
+  "id: Acts ==> \
 \       leadsTo Acts (A Un B) C  =  (leadsTo Acts A C & leadsTo Acts B C)";
 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
 qed "leadsTo_Un_distrib";
 
 Goal
-  "!!C. id: Acts ==> \
+  "id: Acts ==> \
 \       leadsTo Acts (UN i:I. A i) B  =  (ALL i : I. leadsTo Acts (A i) B)";
 by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
 qed "leadsTo_UN_distrib";
 
 Goal
-  "!!C. id: Acts ==> \
+  "id: Acts ==> \
 \       leadsTo Acts (Union S) B  =  (ALL A : S. leadsTo Acts A B)";
 by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
 qed "leadsTo_Union_distrib";
 
 
 Goal
-   "!!Acts. [| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
+   "[| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
 \           ==> leadsTo Acts B B'";
 (*PROOF FAILED: why?*)
 by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
@@ -184,7 +184,7 @@
 
 (*Set difference: maybe combine with leadsTo_weaken_L??*)
 Goal
-  "!!C. [| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
+  "[| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
 \       ==> leadsTo Acts A C";
 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
 qed "leadsTo_Diff";
@@ -212,14 +212,14 @@
 
 (*Version with no index set*)
 Goal
-   "!!Acts. ALL i. leadsTo Acts (A i) (A' i) \
+   "ALL i. leadsTo Acts (A i) (A' i) \
 \           ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
 qed "all_leadsTo_UN_UN";
 
 
 (*Binary union version*)
-Goal "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \
+Goal "[| leadsTo Acts A A'; leadsTo Acts B B' |] \
 \                 ==> leadsTo Acts (A Un B) (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un, 
 			       leadsTo_weaken_R]) 1);
@@ -229,14 +229,14 @@
 (** The cancellation law **)
 
 Goal
-   "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
+   "[| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
 \           ==> leadsTo Acts A (A' Un B')";
 by (blast_tac (claset() addIs [leadsTo_Un_Un, 
 			       subset_imp_leadsTo, leadsTo_Trans]) 1);
 qed "leadsTo_cancel2";
 
 Goal
-   "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
+   "[| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
 \           ==> leadsTo Acts A (A' Un B')";
 by (rtac leadsTo_cancel2 1);
 by (assume_tac 2);
@@ -244,14 +244,14 @@
 qed "leadsTo_cancel_Diff2";
 
 Goal
-   "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
+   "[| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
 \           ==> leadsTo Acts A (B' Un A')";
 by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
 by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
 qed "leadsTo_cancel1";
 
 Goal
-   "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
+   "[| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
 \           ==> leadsTo Acts A (B' Un A')";
 by (rtac leadsTo_cancel1 1);
 by (assume_tac 2);
@@ -262,14 +262,14 @@
 
 (** The impossibility law **)
 
-Goal "!!Acts. leadsTo Acts A B ==> B={} --> A={}";
+Goal "leadsTo Acts A B ==> B={} --> A={}";
 by (etac leadsTo_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
 by (Blast_tac 1);
 val lemma = result() RS mp;
 
-Goal "!!Acts. leadsTo Acts A {} ==> A={}";
+Goal "leadsTo Acts A {} ==> A={}";
 by (blast_tac (claset() addSIs [lemma]) 1);
 qed "leadsTo_empty";
 
@@ -278,7 +278,7 @@
 
 (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
 Goalw [stable_def]
-   "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
+   "[| leadsTo Acts A A'; stable Acts B |] \
 \           ==> leadsTo Acts (A Int B) (A' Int B)";
 by (etac leadsTo_induct 1);
 by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
@@ -292,14 +292,14 @@
 qed "PSP_stable";
 
 Goal
-   "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
+   "[| leadsTo Acts A A'; stable Acts B |] \
 \           ==> leadsTo Acts (B Int A) (B Int A')";
 by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
 qed "PSP_stable2";
 
 
 Goalw [ensures_def]
-   "!!Acts. [| ensures Acts A A'; constrains Acts B B' |] \
+   "[| ensures Acts A A'; constrains Acts B B' |] \
 \           ==> ensures Acts (A Int B) ((A' Int B) Un (B' - B))";
 by Safe_tac;
 by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
@@ -309,7 +309,7 @@
 
 
 Goal
-   "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+   "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
 \           ==> leadsTo Acts (A Int B) ((A' Int B) Un (B' - B))";
 by (etac leadsTo_induct 1);
 by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
@@ -324,14 +324,14 @@
 qed "PSP";
 
 Goal
-   "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+   "[| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
 \           ==> leadsTo Acts (B Int A) ((B Int A') Un (B' - B))";
 by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
 qed "PSP2";
 
 
 Goalw [unless_def]
-   "!!Acts. [| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \
+   "[| leadsTo Acts A A'; unless Acts B B'; id: Acts |] \
 \           ==> leadsTo Acts (A Int B) ((A' Int B) Un B')";
 by (dtac PSP 1);
 by (assume_tac 1);
@@ -346,7 +346,7 @@
 (*** Proving the induction rules ***)
 
 Goal
-   "!!Acts. [| wf r;     \
+   "[| wf r;     \
 \              ALL m. leadsTo Acts (A Int f-``{m})                     \
 \                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \              id: Acts |] \
@@ -362,7 +362,7 @@
 
 (** Meta or object quantifier ????? **)
 Goal
-   "!!Acts. [| wf r;     \
+   "[| wf r;     \
 \              ALL m. leadsTo Acts (A Int f-``{m})                     \
 \                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \              id: Acts |] \
@@ -376,7 +376,7 @@
 
 
 Goal
-   "!!Acts. [| wf r;     \
+   "[| wf r;     \
 \              ALL m:I. leadsTo Acts (A Int f-``{m})                   \
 \                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \              id: Acts |] \
@@ -391,7 +391,7 @@
 
 (*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*)
 Goal
-   "!!Acts. [| ALL m. leadsTo Acts (A Int f-``{m})                     \
+   "[| ALL m. leadsTo Acts (A Int f-``{m})                     \
 \                                  ((A Int f-``(lessThan m)) Un B);   \
 \              id: Acts |] \
 \           ==> leadsTo Acts A B";
@@ -401,7 +401,7 @@
 qed "lessThan_induct";
 
 Goal
-   "!!Acts. [| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m})   \
+   "[| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m})   \
 \                                        ((A Int f-``(lessThan m)) Un B);   \
 \              id: Acts |] \
 \           ==> leadsTo Acts A ((A Int (f-``(atMost l))) Un B)";
@@ -412,7 +412,7 @@
 qed "lessThan_bounded_induct";
 
 Goal
-   "!!Acts. [| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m})   \
+   "[| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m})   \
 \                                    ((A Int f-``(greaterThan m)) Un B);   \
 \              id: Acts |] \
 \           ==> leadsTo Acts A ((A Int (f-``(atLeast l))) Un B)";
@@ -435,18 +435,18 @@
 by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
 qed "wlt_leadsTo";
 
-Goalw [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";
+Goalw [wlt_def] "leadsTo Acts A B ==> A <= wlt Acts B";
 by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
 qed "leadsTo_subset";
 
 (*Misra's property W2*)
-Goal "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";
+Goal "id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";
 by (blast_tac (claset() addSIs [leadsTo_subset, 
 				wlt_leadsTo RS leadsTo_weaken_L]) 1);
 qed "leadsTo_eq_subset_wlt";
 
 (*Misra's property W4*)
-Goal "!!Acts. id: Acts ==> B <= wlt Acts B";
+Goal "id: Acts ==> B <= wlt Acts B";
 by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
 				      subset_imp_leadsTo]) 1);
 qed "wlt_increasing";
@@ -454,7 +454,7 @@
 
 (*Used in the Trans case below*)
 Goalw [constrains_def]
-   "!!Acts. [| B <= A2;  \
+   "[| B <= A2;  \
 \              constrains Acts (A1 - B) (A1 Un B); \
 \              constrains Acts (A2 - C) (A2 Un C) |] \
 \           ==> constrains Acts (A1 Un A2 - C) (A1 Un A2 Un C)";
@@ -465,7 +465,7 @@
 
 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
 Goal
-   "!!Acts. [| leadsTo Acts A A';  id: Acts |] ==> \
+   "[| leadsTo Acts A A';  id: Acts |] ==> \
 \      EX B. A<=B & leadsTo Acts B A' & constrains Acts (B-A') (B Un A')";
 by (etac leadsTo_induct 1);
 (*Basis*)
@@ -485,7 +485,7 @@
 
 
 (*Misra's property W5*)
-Goal "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
+Goal "id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
 by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
 by (Clarify_tac 1);
 by (subgoal_tac "Ba = wlt Acts B" 1);
@@ -498,7 +498,7 @@
 (*** Completion: Binary and General Finite versions ***)
 
 Goal
-   "!!Acts. [| leadsTo Acts A A';  stable Acts A';   \
+   "[| leadsTo Acts A A';  stable Acts A';   \
 \              leadsTo Acts B B';  stable Acts B';  id: Acts |] \
 \           ==> leadsTo Acts (A Int B) (A' Int B')";
 by (subgoal_tac "stable Acts (wlt Acts B')" 1);
@@ -520,7 +520,7 @@
 
 
 Goal
-   "!!Acts. [| finite I;  id: Acts |]                     \
+   "[| finite I;  id: Acts |]                     \
 \           ==> (ALL i:I. leadsTo Acts (A i) (A' i)) -->  \
 \               (ALL i:I. stable Acts (A' i)) -->         \
 \               leadsTo Acts (INT i:I. A i) (INT i:I. A' i)";
@@ -533,7 +533,7 @@
 
 
 Goal
-   "!!Acts. [| W = wlt Acts (B' Un C);     \
+   "[| W = wlt Acts (B' Un C);     \
 \              leadsTo Acts A (A' Un C);  constrains Acts A' (A' Un C);   \
 \              leadsTo Acts B (B' Un C);  constrains Acts B' (B' Un C);   \
 \              id: Acts |] \
@@ -563,7 +563,7 @@
 
 
 Goal
-   "!!Acts. [| finite I;  id: Acts |] \
+   "[| finite I;  id: Acts |] \
 \           ==> (ALL i:I. leadsTo Acts (A i) (A' i Un C)) -->  \
 \               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
 \               leadsTo Acts (INT i:I. A i) ((INT i:I. A' i) Un C)";