Removed leading !! in goals.

--- a/src/HOL/IMP/Denotation.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/IMP/Denotation.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -25,7 +25,7 @@
 
 (* Operational Semantics implies Denotational Semantics *)
 
-Goal "!!c s t. <c,s> -c-> t ==> (s,t) : C(c)";
+Goal "<c,s> -c-> t ==> (s,t) : C(c)";
 
 (* start with rule induction *)
 by (etac evalc.induct 1);

--- a/src/HOL/IMP/Hoare.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -9,7 +9,7 @@
 
 open Hoare;
 
-Goalw [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
+Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";
 by (etac hoare.induct 1);
     by (ALLGOALS Asm_simp_tac);
   by (Fast_tac 1);
@@ -38,20 +38,19 @@
 qed "wp_Semi";
 
 Goalw [wp_def]
-  "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & \
-\                                    (~b s --> wp d Q s))";
+ "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))";
 by (Simp_tac 1);
 by (rtac ext 1);
 by (Fast_tac 1);
 qed "wp_If";
 
 Goalw [wp_def]
-  "!!s. b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
+  "b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
 qed "wp_While_True";
 
-Goalw [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
+Goalw [wp_def] "~b s ==> wp (WHILE b DO c) Q s = Q s";
 by (stac C_While_If 1);
 by (Asm_simp_tac 1);
 qed "wp_While_False";
@@ -59,8 +58,8 @@
 Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
 
 (*Not suitable for rewriting: LOOPS!*)
-Goal "wp (WHILE b DO c) Q s = \
-\                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
+Goal
+ "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
 by (Simp_tac 1);
 qed "wp_While_if";
 
@@ -114,7 +113,7 @@
 by (Asm_full_simp_tac 1);
 qed_spec_mp "wp_is_pre";
 
-Goal "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
+Goal "|= {P}c{Q} ==> |- {P}c{Q}";
 by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
  by (Fast_tac 2);
 by (rewrite_goals_tac [hoare_valid_def,wp_def]);

--- a/src/HOL/IMP/Natural.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/IMP/Natural.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -17,7 +17,7 @@
 AddSEs evalc_elim_cases;
 
 (* evaluation of com is deterministic *)
-Goal "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
+Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
 by (etac evalc.induct 1);
 by (thin_tac "<?c,s2> -c-> s1" 7);
 (*blast_tac needs Unify.search_bound, trace_bound := 40*)

--- a/src/HOL/IMP/Transition.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/IMP/Transition.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -22,7 +22,7 @@
 
 AddIs evalc1.intrs;
 
-Goal "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
+Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
 by (etac rel_pow_E2 1);
 by (Asm_full_simp_tac 1);
 by (Fast_tac 1);
@@ -38,7 +38,7 @@
 qed_spec_mp "lemma1";
 
 
-Goal "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
+Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
 by (etac evalc.induct 1);
 
 (* SKIP *)
@@ -120,7 +120,7 @@
 section "A Proof Without -n->";
 
 Goal
- "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
+ "(c1,s1) -*-> (SKIP,s2) ==> \
 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
 by (etac converse_rtrancl_induct2 1);
 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
@@ -128,7 +128,7 @@
 qed_spec_mp "my_lemma1";
 
 
-Goal "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
+Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
 by (etac evalc.induct 1);
 
 (* SKIP *)
@@ -186,7 +186,7 @@
 
 (*Delsimps [update_apply];*)
 Goal 
-  "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
+  "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
 by (etac evalc1.induct 1);
 by Auto_tac;
 qed_spec_mp "FB_lemma3";
@@ -199,6 +199,6 @@
 by (fast_tac (claset() addIs [FB_lemma3]) 1);
 qed_spec_mp "FB_lemma2";
 
-Goal "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
+Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
 by (fast_tac (claset() addEs [FB_lemma2]) 1);
 qed "evalc1_impl_evalc";

--- a/src/HOL/IMP/VC.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/IMP/VC.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -46,8 +46,8 @@
 qed_spec_mp "vc_mono";
 
 Goal
-  "!!P c Q. |- {P}c{Q} ==> \
-\          (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
+  "|- {P}c{Q} ==> \
+\  (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
 by (etac hoare.induct 1);
      by (res_inst_tac [("x","Askip")] exI 1);
      by (Simp_tac 1);
@@ -61,7 +61,7 @@
   by (res_inst_tac [("x","Aif b ac aca")] exI 1);
   by (Asm_simp_tac 1);
  by (SELECT_GOAL(safe_tac HOL_cs)1);
- by (res_inst_tac [("x","Awhile b Pa ac")] exI 1);
+ by (res_inst_tac [("x","Awhile b P ac")] exI 1);
  by (Asm_simp_tac 1);
 by (safe_tac HOL_cs);
 by (res_inst_tac [("x","ac")] exI 1);

--- a/src/HOL/Lambda/Commutation.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -10,22 +10,22 @@
 
 (*** square ***)
 
-Goalw [square_def] "!!R. square R S T U ==> square S R U T";
+Goalw [square_def] "square R S T U ==> square S R U T";
 by (Blast_tac 1);
 qed "square_sym";
 
 Goalw [square_def]
-  "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
+  "[| square R S T U; T <= T' |] ==> square R S T' U";
 by (Blast_tac 1);
 qed "square_subset";
 
 Goalw [square_def]
-  "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
+  "[| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
 by (Blast_tac 1);
 qed "square_reflcl";
 
 Goalw [square_def]
-  "!!R. square R S S T ==> square (R^*) S S (T^*)";
+  "square R S S T ==> square (R^*) S S (T^*)";
 by (strip_tac 1);
 by (etac rtrancl_induct 1);
 by (Blast_tac 1);
@@ -33,7 +33,7 @@
 qed "square_rtrancl";
 
 Goalw [commute_def]
- "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
+ "square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
 by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
                        addEs [r_into_rtrancl]
                        addss simpset()) 1);
@@ -41,45 +41,43 @@
 
 (*** commute ***)
 
-Goalw [commute_def] "!!R. commute R S ==> commute S R";
+Goalw [commute_def] "commute R S ==> commute S R";
 by (blast_tac (claset() addIs [square_sym]) 1);
 qed "commute_sym";
 
-Goalw [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
+Goalw [commute_def] "commute R S ==> commute (R^*) (S^*)";
 by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1);
 qed "commute_rtrancl";
 
 Goalw [commute_def,square_def]
-  "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
+  "[| commute R T; commute S T |] ==> commute (R Un S) T";
 by (Blast_tac 1);
 qed "commute_Un";
 
 (*** diamond, confluence and union ***)
 
 Goalw [diamond_def]
-  "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
+  "[| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
 by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
 qed "diamond_Un";
 
-Goalw [diamond_def] "!!R. diamond R ==> confluent (R)";
+Goalw [diamond_def] "diamond R ==> confluent (R)";
 by (etac commute_rtrancl 1);
 qed "diamond_confluent";
 
 Goalw [diamond_def]
-  "!!R. square R R (R^=) (R^=) ==> confluent R";
+  "square R R (R^=) (R^=) ==> confluent R";
 by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
                        addEs [square_subset]) 1);
 qed "square_reflcl_confluent";
 
 Goal
- "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
-\      ==> confluent(R Un S)";
+ "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent(R Un S)";
 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
 by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
 qed "confluent_Un";
 
-Goal
-  "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
+Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
 by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] 
 		       addss simpset()) 1);
 qed "diamond_to_confluence";

--- a/src/HOL/Lambda/Eta.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -32,8 +32,7 @@
 qed_spec_mp "subst_not_free";
 Addsimps [subst_not_free RS eqTrueI];
 
-Goal "!i k. free (lift t k) i = \
-\                   (i < k & free t i | k < i & free t (i-1))";
+Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
 by (Blast_tac 2);
@@ -56,16 +55,16 @@
 qed "free_subst";
 Addsimps [free_subst];
 
-Goal "!!s. s -e> t ==> !i. free t i = free s i";
+Goal "s -e> t ==> !i. free t i = free s i";
 by (etac eta.induct 1);
 by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong])));
 qed_spec_mp "free_eta";
 
-Goal "!!s. [| s -e> t; ~free s i |] ==> ~free t i";
+Goal "[| s -e> t; ~free s i |] ==> ~free t i";
 by (asm_simp_tac (simpset() addsimps [free_eta]) 1);
 qed "not_free_eta";
 
-Goal "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
+Goal "s -e> t ==> !u i. s[u/i] -e> t[u/i]";
 by (etac eta.induct 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
 qed_spec_mp "eta_subst";
@@ -90,34 +89,34 @@
 
 section "Congruence rules for -e>>";
 
-Goal "!!s. s -e>> s' ==> Abs s -e>> Abs s'";
+Goal "s -e>> s' ==> Abs s -e>> Abs s'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_Abs";
 
-Goal "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
+Goal "s -e>> s' ==> s @ t -e>> s' @ t";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppL";
 
-Goal "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
+Goal "t -e>> t' ==> s @ t -e>> s @ t'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
 qed "rtrancl_eta_AppR";
 
-Goal "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
+Goal "[| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
 by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
                        addIs [rtrancl_trans]) 1);
 qed "rtrancl_eta_App";
 
 section "Commutation of -> and -e>";
 
-Goal "!!s t. s -> t ==> (!i. free t i --> free s i)";
+Goal "s -> t ==> (!i. free t i --> free s i)";
 by (etac beta.induct 1);
 by (ALLGOALS(Asm_full_simp_tac));
 qed_spec_mp "free_beta";
 
-Goal "!!s t. s -> t ==> !u i. s[u/i] -> t[u/i]";
+Goal "s -> t ==> !u i. s[u/i] -> t[u/i]";
 by (etac beta.induct 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym])));
 qed_spec_mp "beta_subst";
@@ -131,7 +130,7 @@
 qed_spec_mp "subst_Var_Suc";
 Addsimps [subst_Var_Suc];
 
-Goal "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)";
+Goal "s -e> t ==> (!i. lift s i -e> lift t i)";
 by (etac eta.induct 1);
 by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
 qed_spec_mp "eta_lift";
@@ -216,6 +215,6 @@
 qed_spec_mp "not_free_iff_lifted";
 
 Goal "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
-\             (!s. R(Abs(lift s 0 @ Var 0))(s))";
+\     (!s. R(Abs(lift s 0 @ Var 0))(s))";
 by (fast_tac (HOL_cs addss (simpset() addsimps [not_free_iff_lifted])) 1);
 qed "explicit_is_implicit";

--- a/src/HOL/Lambda/Lambda.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -21,23 +21,23 @@
 
 (*** Congruence rules for ->> ***)
 
-Goal "!!s. s ->> s' ==> Abs s ->> Abs s'";
+Goal "s ->> s' ==> Abs s ->> Abs s'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_Abs";
 AddSIs [rtrancl_beta_Abs];
 
-Goal "!!s. s ->> s' ==> s @ t ->> s' @ t";
+Goal "s ->> s' ==> s @ t ->> s' @ t";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppL";
 
-Goal "!!s. t ->> t' ==> s @ t ->> s @ t'";
+Goal "t ->> t' ==> s @ t ->> s @ t'";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_beta_AppR";
 
-Goal "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
+Goal "[| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
 by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
                        addIs  [rtrancl_trans]) 1);
 qed "rtrancl_beta_App";
@@ -53,11 +53,11 @@
 by (asm_full_simp_tac(addsplit(simpset())) 1);
 qed "subst_eq";
 
-Goal "!!s. i<j ==> (Var j)[u/i] = Var(j-1)";
+Goal "i<j ==> (Var j)[u/i] = Var(j-1)";
 by (asm_full_simp_tac(addsplit(simpset())) 1);
 qed "subst_gt";
 
-Goal "!!s. j<i ==> (Var j)[u/i] = Var(j)";
+Goal "j<i ==> (Var j)[u/i] = Var(j)";
 by (asm_full_simp_tac (addsplit(simpset()) addsimps
                           [less_not_refl2 RS not_sym,less_SucI]) 1);
 qed "subst_lt";
@@ -72,8 +72,7 @@
 by (ALLGOALS trans_tac);
 qed_spec_mp "lift_lift";
 
-Goal "!i j s. j < Suc i --> \
-\         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
+Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
                                 addsplits [split_nat_case]
@@ -84,8 +83,7 @@
 Addsimps [lift_subst];
 
 Goal
-  "!i j s. i < Suc j -->\
-\         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
+  "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
                                 addSolver cut_trans_tac)));
@@ -100,8 +98,7 @@
 Addsimps [subst_lift];
 
 
-Goal "!i j u v. i < Suc j --> \
-\ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
+Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]