# HG changeset patch
# User paulson
# Date 900490513 -7200
# Node ID b94cd208f0739da6349148ad6b476c87d42f6932
# Parent  c56aa8b59dc0da1c2349587a0e4eded3d538560e
Removal of leading "\!\!..." from most Goal commands

diff -r c56aa8b59dc0 -r b94cd208f073 src/CCL/Set.ML
--- a/src/CCL/Set.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/CCL/Set.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -116,7 +116,7 @@
 qed_goal "subset_refl" Set.thy "A <= A"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
-Goal "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
+Goal "[| A<=B;  B<=C |] ==> A<=C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
 qed "subset_trans";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Arith.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -28,7 +28,7 @@
 (* Could be (and is, below) generalized in various ways;
    However, none of the generalizations are currently in the simpset,
    and I dread to think what happens if I put them in *)
-Goal "!!n. 0 < n ==> Suc(n-1) = n";
+Goal "0 < n ==> Suc(n-1) = n";
 by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
 qed "Suc_pred";
 Addsimps [Suc_pred];
@@ -111,7 +111,7 @@
 Addsimps [pred_add_is_0];
 
 (* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
-Goal "!!n. 0<n ==> m + (n-1) = (m+n)-1";
+Goal "0<n ==> m + (n-1) = (m+n)-1";
 by (exhaust_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
                                       addsplits [split_nat_case])));
@@ -128,7 +128,7 @@
 (**** Additional theorems about "less than" ****)
 
 (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
-Goal "!!m. m<n --> (? k. n=Suc(m+k))";
+Goal "m<n --> (? k. n=Suc(m+k))";
 by (induct_tac "n" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
 by (blast_tac (claset() addSEs [less_SucE] 
@@ -162,7 +162,7 @@
 (*"i < j ==> i < m+j"*)
 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
 
-Goal "!!i. i+j < (k::nat) ==> i<k";
+Goal "i+j < (k::nat) ==> i<k";
 by (etac rev_mp 1);
 by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -328,11 +328,11 @@
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "add_diff_inverse";
 
-Goal "!!m. n<=m ==> n+(m-n) = (m::nat)";
+Goal "n<=m ==> n+(m-n) = (m::nat)";
 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
 qed "le_add_diff_inverse";
 
-Goal "!!m. n<=m ==> (m-n)+n = (m::nat)";
+Goal "n<=m ==> (m-n)+n = (m::nat)";
 by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
 qed "le_add_diff_inverse2";
 
@@ -372,7 +372,7 @@
 qed "Suc_diff_diff";
 Addsimps [Suc_diff_diff];
 
-Goal "!!n. 0<n ==> n - Suc i < n";
+Goal "0<n ==> n - Suc i < n";
 by (res_inst_tac [("n","n")] natE 1);
 by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
@@ -557,13 +557,13 @@
 qed "mult_eq_1_iff";
 Addsimps [mult_eq_1_iff];
 
-Goal "!!k. 0<k ==> (m*k < n*k) = (m<n)";
+Goal "0<k ==> (m*k < n*k) = (m<n)";
 by (safe_tac (claset() addSIs [mult_less_mono1]));
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
 qed "mult_less_cancel2";
 
-Goal "!!k. 0<k ==> (k*m < k*n) = (m<n)";
+Goal "0<k ==> (k*m < k*n) = (m<n)";
 by (dtac mult_less_cancel2 1);
 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
 qed "mult_less_cancel1";
@@ -579,7 +579,7 @@
 by (rtac Suc_mult_less_cancel1 1);
 qed "Suc_mult_le_cancel1";
 
-Goal "!!k. 0<k ==> (m*k = n*k) = (m=n)";
+Goal "0<k ==> (m*k = n*k) = (m=n)";
 by (cut_facts_tac [less_linear] 1);
 by Safe_tac;
 by (assume_tac 2);
@@ -587,7 +587,7 @@
 by (ALLGOALS Asm_full_simp_tac);
 qed "mult_cancel2";
 
-Goal "!!k. 0<k ==> (k*m = k*n) = (m=n)";
+Goal "0<k ==> (k*m = k*n) = (m=n)";
 by (dtac mult_cancel2 1);
 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
 qed "mult_cancel1";
@@ -601,7 +601,7 @@
 
 (** Lemma for gcd **)
 
-Goal "!!m n. m = m*n ==> n=1 | m=0";
+Goal "m = m*n ==> n=1 | m=0";
 by (dtac sym 1);
 by (rtac disjCI 1);
 by (rtac nat_less_cases 1 THEN assume_tac 2);
@@ -626,11 +626,11 @@
 by (Asm_full_simp_tac 1);
 qed "add_less_imp_less_diff";
 
-Goal "!! n. n <= m ==> Suc m - n = Suc (m - n)";
+Goal "n <= m ==> Suc m - n = Suc (m - n)";
 by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
 qed "Suc_diff_le";
 
-Goal "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
+Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
 by (asm_full_simp_tac
     (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
 qed "Suc_diff_Suc";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Divides.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -27,18 +27,18 @@
 by (simp_tac (simpset() addsimps [mod_def]) 1);
 qed "mod_eq";
 
-Goal "!!m. m<n ==> m mod n = m";
+Goal "m<n ==> m mod n = m";
 by (rtac (mod_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "mod_less";
 
-Goal "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
+Goal "[| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
 by (rtac (mod_eq RS wf_less_trans) 1);
 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "mod_geq";
 
 (*NOT suitable for rewriting: loops*)
-Goal "!!m. 0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
+Goal "0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
 qed "mod_if";
 
@@ -48,17 +48,17 @@
 qed "mod_1";
 Addsimps [mod_1];
 
-Goal "!!n. 0<n ==> n mod n = 0";
+Goal "0<n ==> n mod n = 0";
 by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
 qed "mod_self";
 
-Goal "!!n. 0<n ==> (m+n) mod n = m mod n";
+Goal "0<n ==> (m+n) mod n = m mod n";
 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
 by (stac (mod_geq RS sym) 2);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
 qed "mod_add_self2";
 
-Goal "!!k. 0<n ==> (n+m) mod n = m mod n";
+Goal "0<n ==> (n+m) mod n = m mod n";
 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
 qed "mod_add_self1";
 
@@ -67,13 +67,13 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1]))));
 qed "mod_mult_self1";
 
-Goal "!!m. 0<n ==> (m + n*k) mod n = m mod n";
+Goal "0<n ==> (m + n*k) mod n = m mod n";
 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
 qed "mod_mult_self2";
 
 Addsimps [mod_mult_self1, mod_mult_self2];
 
-Goal "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
+Goal "[| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (stac mod_if 1);
 by (Asm_simp_tac 1);
@@ -81,7 +81,7 @@
 				      diff_less, diff_mult_distrib]) 1);
 qed "mod_mult_distrib";
 
-Goal "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
+Goal "[| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (stac mod_if 1);
 by (Asm_simp_tac 1);
@@ -89,7 +89,7 @@
 				      diff_less, diff_mult_distrib2]) 1);
 qed "mod_mult_distrib2";
 
-Goal "!!n. 0<n ==> m*n mod n = 0";
+Goal "0<n ==> m*n mod n = 0";
 by (induct_tac "m" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
 by (dres_inst_tac [("m","m*n")] mod_add_self2 1);
@@ -104,23 +104,23 @@
 by (simp_tac (simpset() addsimps [div_def]) 1);
 qed "div_eq";
 
-Goal "!!m. m<n ==> m div n = 0";
+Goal "m<n ==> m div n = 0";
 by (rtac (div_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "div_less";
 
-Goal "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
+Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
 by (rtac (div_eq RS wf_less_trans) 1);
 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "div_geq";
 
 (*NOT suitable for rewriting: loops*)
-Goal "!!m. 0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
+Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
 qed "div_if";
 
 (*Main Result about quotient and remainder.*)
-Goal "!!m. 0<n ==> (m div n)*n + m mod n = m";
+Goal "0<n ==> (m div n)*n + m mod n = m";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (stac mod_if 1);
 by (ALLGOALS (asm_simp_tac 
@@ -130,7 +130,7 @@
 qed "mod_div_equality";
 
 (* a simple rearrangement of mod_div_equality: *)
-Goal "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
+Goal "0<k ==> k*(m div k) = m - (m mod k)";
 by (dres_inst_tac [("m","m")] mod_div_equality 1);
 by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
            K(IF_UNSOLVED no_tac)]);
@@ -142,18 +142,18 @@
 qed "div_1";
 Addsimps [div_1];
 
-Goal "!!n. 0<n ==> n div n = 1";
+Goal "0<n ==> n div n = 1";
 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
 qed "div_self";
 
 
-Goal "!!n. 0<n ==> (m+n) div n = Suc (m div n)";
+Goal "0<n ==> (m+n) div n = Suc (m div n)";
 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
 by (stac (div_geq RS sym) 2);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
 qed "div_add_self2";
 
-Goal "!!k. 0<n ==> (n+m) div n = Suc (m div n)";
+Goal "0<n ==> (n+m) div n = Suc (m div n)";
 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
 qed "div_add_self1";
 
@@ -162,7 +162,7 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1]))));
 qed "div_mult_self1";
 
-Goal "!!m. 0<n ==> (m + n*k) div n = k + m div n";
+Goal "0<n ==> (m + n*k) div n = k + m div n";
 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
 qed "div_mult_self2";
 
@@ -170,10 +170,10 @@
 
 
 (* Monotonicity of div in first argument *)
-Goal "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
+Goal "0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
 by (res_inst_tac [("n","n")] less_induct 1);
 by (Clarify_tac 1);
-by (case_tac "na<k" 1);
+by (case_tac "n<k" 1);
 (* 1  case n<k *)
 by (subgoal_tac "m<k" 1);
 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
@@ -188,7 +188,7 @@
 
 
 (* Antimonotonicity of div in second argument *)
-Goal "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
+Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
 by (subgoal_tac "0<n" 1);
  by (trans_tac 2);
 by (res_inst_tac [("n","k")] less_induct 1);
@@ -205,7 +205,7 @@
 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
 qed "div_le_mono2";
 
-Goal "!!m n. 0<n ==> m div n <= m";
+Goal "0<n ==> m div n <= m";
 by (subgoal_tac "m div n <= m div 1" 1);
 by (Asm_full_simp_tac 1);
 by (rtac div_le_mono2 1);
@@ -214,7 +214,7 @@
 Addsimps [div_le_dividend];
 
 (* Similar for "less than" *)
-Goal "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
+Goal "1<n ==> (0 < m) --> (m div n < m)";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (Simp_tac 1);
 by (rename_tac "m" 1);
@@ -255,7 +255,7 @@
 by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
 qed "mod_Suc";
 
-Goal "!!m n. 0<n ==> m mod n < n";
+Goal "0<n ==> m mod n < n";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (excluded_middle_tac "na<n" 1);
 (*case na<n*)
@@ -270,7 +270,7 @@
 (*With less_zeroE, causes case analysis on b<2*)
 AddSEs [less_SucE];
 
-Goal "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
+Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
 by (subgoal_tac "k mod 2 < 2" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
 by (Asm_simp_tac 1);
@@ -311,7 +311,7 @@
 
 (*** More division laws ***)
 
-Goal "!!n. 0<n ==> m*n div n = m";
+Goal "0<n ==> m*n div n = m";
 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
@@ -319,7 +319,7 @@
 Addsimps [div_mult_self_is_m];
 
 (*Cancellation law for division*)
-Goal "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
+Goal "[| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (case_tac "na<n" 1);
 by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
@@ -333,7 +333,7 @@
 qed "div_cancel";
 Addsimps [div_cancel];
 
-Goal "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
+Goal "[| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (case_tac "na<n" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
@@ -356,7 +356,7 @@
 qed "dvd_0_right";
 Addsimps [dvd_0_right];
 
-Goalw [dvd_def] "!!m. 0 dvd m ==> m = 0";
+Goalw [dvd_def] "0 dvd m ==> m = 0";
 by (fast_tac (claset() addss simpset()) 1);
 qed "dvd_0_left";
 
@@ -370,33 +370,33 @@
 qed "dvd_refl";
 Addsimps [dvd_refl];
 
-Goalw [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
+Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
 by (blast_tac (claset() addIs [mult_assoc] ) 1);
 qed "dvd_trans";
 
-Goalw [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
+Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
 by (fast_tac (claset() addDs [mult_eq_self_implies_10]
                      addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
 qed "dvd_anti_sym";
 
-Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
 qed "dvd_add";
 
-Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)";
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
 qed "dvd_diff";
 
-Goal "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
+Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
 by (blast_tac (claset() addIs [dvd_add]) 1);
 qed "dvd_diffD";
 
-Goalw [dvd_def] "!!k. k dvd n ==> k dvd (m*n)";
+Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
 by (blast_tac (claset() addIs [mult_left_commute]) 1);
 qed "dvd_mult";
 
-Goal "!!k. k dvd m ==> k dvd (m*n)";
+Goal "k dvd m ==> k dvd (m*n)";
 by (stac mult_commute 1);
 by (etac dvd_mult 1);
 qed "dvd_mult2";
@@ -404,7 +404,7 @@
 (* k dvd (m*k) *)
 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
 
-Goalw [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
+Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
 by (Clarify_tac 1);
 by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
 by (res_inst_tac 
@@ -414,30 +414,30 @@
                                      mult_mod_distrib, add_mult_distrib2]) 1);
 qed "dvd_mod";
 
-Goal "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
+Goal "[| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
 qed "dvd_mod_imp_dvd";
 
-Goalw [dvd_def]  "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
+Goalw [dvd_def]  "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
 by (etac exE 1);
 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
 by (Blast_tac 1);
 qed "dvd_mult_cancel";
 
-Goalw [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
+Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
 by (Clarify_tac 1);
 by (res_inst_tac [("x","k*ka")] exI 1);
 by (asm_simp_tac (simpset() addsimps mult_ac) 1);
 qed "mult_dvd_mono";
 
-Goalw [dvd_def] "!!c. (i*j) dvd k ==> i dvd k";
+Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
 by (Blast_tac 1);
 qed "dvd_mult_left";
 
-Goalw [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
+Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
 by (Clarify_tac 1);
 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
 by (etac conjE 1);
@@ -447,11 +447,11 @@
 by (Simp_tac 1);
 qed "dvd_imp_le";
 
-Goalw [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
+Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)";
 by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
+by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
 by (stac mult_commute 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
-by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
 by (Blast_tac 1);
 qed "dvd_eq_mod_eq_0";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Finite.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -42,7 +42,7 @@
 qed "finite_UnI";
 
 (*Every subset of a finite set is finite*)
-Goal "!!B. finite B ==> ALL A. A<=B --> finite A";
+Goal "finite B ==> ALL A. A<=B --> finite A";
 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
@@ -50,7 +50,7 @@
 by (ALLGOALS Asm_simp_tac);
 val lemma = result();
 
-Goal "!!A. [| A<=B;  finite B |] ==> finite A";
+Goal "[| A<=B;  finite B |] ==> finite A";
 by (dtac lemma 1);
 by (Blast_tac 1);
 qed "finite_subset";
@@ -70,7 +70,7 @@
 Addsimps[finite_insert];
 
 (*The image of a finite set is finite *)
-Goal  "!!F. finite F ==> finite(h``F)";
+Goal  "finite F ==> finite(h``F)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -111,7 +111,7 @@
 AddIffs [finite_Diff_singleton];
 
 (*Lemma for proving finite_imageD*)
-Goal "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A";
+Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
@@ -127,7 +127,7 @@
     (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
 val lemma = result();
 
-Goal "!!A. [| finite(f``A);  inj_on f A |] ==> finite A";
+Goal "[| finite(f``A);  inj_on f A |] ==> finite A";
 by (dtac lemma 1);
 by (Blast_tac 1);
 qed "finite_imageD";
@@ -151,7 +151,7 @@
 
 (** The powerset of a finite set **)
 
-Goal "!!A. finite(Pow A) ==> finite A";
+Goal "finite(Pow A) ==> finite A";
 by (subgoal_tac "finite ((%x.{x})``A)" 1);
 by (rtac finite_subset 2);
 by (assume_tac 3);
@@ -273,7 +273,7 @@
 by (Blast_tac 1);
 val lemma = result();
 
-Goal "!!A. [| finite A; x ~: A |] ==> \
+Goal "[| finite A; x ~: A |] ==> \
 \ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
 by (rtac Least_equality 1);
  by (dtac finite_has_card 1);
@@ -309,12 +309,12 @@
 qed "card_insert_disjoint";
 Addsimps [card_insert_disjoint];
 
-Goal "!!A. finite A ==> card A <= card (insert x A)";
+Goal "finite A ==> card A <= card (insert x A)";
 by (case_tac "x: A" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
 qed "card_insert_le";
 
-Goal  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
+Goal  "finite A ==> !B. B <= A --> card(B) <= card(A)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (Clarify_tac 1);
@@ -325,13 +325,13 @@
 	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
 qed_spec_mp "card_mono";
 
-Goal "!!A B. [| finite A; finite B |]\
+Goal "[| finite A; finite B |]\
 \                       ==> A Int B = {} --> card(A Un B) = card A + card B";
 by (etac finite_induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
 qed_spec_mp "card_Un_disjoint";
 
-Goal "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
+Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
 by (subgoal_tac "(A-B) Un B = A" 1);
 by (Blast_tac 2);
 by (rtac (add_right_cancel RS iffD1) 1);
@@ -344,18 +344,18 @@
 			 add_diff_inverse, card_mono, finite_subset])));
 qed "card_Diff_subset";
 
-Goal "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
+Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
 by (assume_tac 1);
 by (Asm_simp_tac 1);
 qed "card_Suc_Diff";
 
-Goal "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
+Goal "[| finite A; x: A |] ==> card(A-{x}) < card A";
 by (rtac Suc_less_SucD 1);
 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
 qed "card_Diff";
 
-Goal "!!A. finite A ==> card(A-{x}) <= card A";
+Goal "finite A ==> card(A-{x}) <= card A";
 by (case_tac "x: A" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le])));
 qed "card_Diff_le";
@@ -363,14 +363,14 @@
 
 (*** Cardinality of the Powerset ***)
 
-Goal "!!A. finite A ==> card(insert x A) = Suc(card(A-{x}))";
+Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
 by (case_tac "x:A" 1);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));
 qed "card_insert";
 Addsimps [card_insert];
 
-Goal "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A";
+Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by Safe_tac;
@@ -382,7 +382,7 @@
 by (Blast_tac 1);
 qed_spec_mp "card_image";
 
-Goal "!!A. finite A ==> card (Pow A) = 2 ^ card A";
+Goal "finite A ==> card (Pow A) = 2 ^ card A";
 by (etac finite_induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
 by (stac card_Un_disjoint 1);
@@ -418,7 +418,7 @@
 
 (*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   The "finite C" premise is redundant*)
-Goal "!!C. finite C ==> finite (Union C) --> \
+Goal "finite C ==> finite (Union C) --> \
 \          (! c : C. k dvd card c) -->  \
 \          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
 \          --> k dvd card(Union C)";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Fun.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -97,7 +97,7 @@
 by (REPEAT (resolve_tac prems 1));
 qed "inj_onD";
 
-Goal "!!x y.[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
+Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
 by (blast_tac (claset() addSDs [inj_onD]) 1);
 qed "inj_on_iff";
 
@@ -135,7 +135,7 @@
 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
 qed "inv_injective";
 
-Goal "!!f. [| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
+Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
 by (fast_tac (claset() addIs [inj_onI] 
                       addEs [inv_injective,injD]) 1);
 qed "inj_on_inv";
@@ -150,11 +150,11 @@
 by (Blast_tac 1);
 qed "inj_on_image_set_diff";
 
-Goalw [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
+Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
 by (Blast_tac 1);
 qed "image_Int";
 
-Goalw [inj_def] "!!f. inj f ==> f``(A-B) = f``A - f``B";
+Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
 by (Blast_tac 1);
 qed "image_set_diff";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/IOA/Asig.ML
--- a/src/HOL/IOA/Asig.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/Asig.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -10,10 +10,10 @@
 
 val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
 
-Goal "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
+Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
 qed"int_and_ext_is_act";
 
-Goal "!!a.[|a:externals(S)|] ==> a:actions(S)";
+Goal "[|a:externals(S)|] ==> a:actions(S)";
 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
 qed"ext_is_act";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/IOA.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -46,7 +46,7 @@
   by (Fast_tac 1);
 qed "mk_trace_thm";
 
-Goalw [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
+Goalw [reachable_def] "s:starts_of(A) ==> reachable A s";
   by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1);
   by (Simp_tac 1);
   by (asm_simp_tac (simpset() addsimps exec_rws) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/IOA/Solve.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -65,7 +65,7 @@
  by (Fast_tac 1);
 val externals_of_par_extra = result(); 
 
-Goal "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
+Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
 by (etac bexE 1);
 by (res_inst_tac [("x",
@@ -85,7 +85,7 @@
 
 (* Exact copy of proof of comp1_reachable for the second 
    component of a parallel composition.     *)
-Goal "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
+Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
 by (etac bexE 1);
 by (res_inst_tac [("x",
@@ -105,7 +105,7 @@
 Delsplits [split_if];
 
 (* Composition of possibility-mappings *)
-Goalw [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
+Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
 \               externals(asig_of(A1))=externals(asig_of(C1)) &\
 \               is_weak_pmap g C2 A2 &  \
 \               externals(asig_of(A2))=externals(asig_of(C2)) & \
@@ -149,7 +149,7 @@
 qed"fxg_is_weak_pmap_of_product_IOA";
 
 
-Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
+Goal "[| reachable (rename C g) s |] ==> reachable C s";
 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
 by (etac bexE 1);
 by (res_inst_tac [("x",
@@ -166,7 +166,7 @@
 qed"reachable_rename_ioa";
 
 
-Goal "!!f.[| is_weak_pmap f C A |]\
+Goal "[| is_weak_pmap f C A |]\
 \                      ==> (is_weak_pmap f (rename C g) (rename A g))";
 by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
 by (rtac conjI 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -18,7 +18,7 @@
                             map (rewrite_rule [pred_def]) acc.intrs)) 1);
 qed "accI";
 
-Goal "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
+Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
 by (etac acc.elim 1);
 by (rewtac pred_def);
 by (Fast_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Com.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -19,7 +19,7 @@
 AddSEs exec_elim_cases;
 
 (*This theorem justifies using "exec" in the inductive definition of "eval"*)
-Goalw exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
+Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "exec_mono";
@@ -29,7 +29,7 @@
 Unify.search_bound := 60;
 
 (*Command execution is functional (deterministic) provided evaluation is*)
-Goal "!!x. Function ev ==> Function(exec ev)";
+Goal "Function ev ==> Function(exec ev)";
 by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
@@ -48,7 +48,7 @@
 by (Simp_tac 1);
 qed "assign_same";
 
-Goalw [assign_def] "!!y. y~=x ==> (s[v/x])y = s y";
+Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
 by (Asm_simp_tac 1);
 qed "assign_different";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Comb.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -55,22 +55,22 @@
 AddIs  [contract.Ap1, contract.Ap2];
 AddSEs [K_contractE, S_contractE, Ap_contractE];
 
-Goalw [I_def] "!!z. I -1-> z ==> P";
+Goalw [I_def] "I -1-> z ==> P";
 by (Blast_tac 1);
 qed "I_contract_E";
 AddSEs [I_contract_E];
 
-Goal "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
+Goal "K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
 by (Blast_tac 1);
 qed "K1_contractD";
 AddSEs [K1_contractD];
 
-Goal "!!x z. x ---> y ==> x#z ---> y#z";
+Goal "x ---> y ==> x#z ---> y#z";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
 qed "Ap_reduce1";
 
-Goal "!!x z. x ---> y ==> z#x ---> z#y";
+Goal "x ---> y ==> z#x ---> z#y";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
 qed "Ap_reduce2";
@@ -108,12 +108,12 @@
 
 (*** Basic properties of parallel contraction ***)
 
-Goal "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
+Goal "K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
 by (Blast_tac 1);
 qed "K1_parcontractD";
 AddSDs [K1_parcontractD];
 
-Goal "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
+Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
 by (Blast_tac 1);
 qed "S1_parcontractD";
 AddSDs [S1_parcontractD];
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Exp.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -97,7 +97,7 @@
 qed "Function_eval";
 
 
-Goal "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
+Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
 by (etac eval_induct 1);
 by (ALLGOALS Asm_simp_tac);
 val lemma = result();
@@ -107,7 +107,7 @@
 
 
 (*This theorem says that "WHILE TRUE DO c" cannot terminate*)
-Goal "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
+Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
 by (etac exec.induct 1);
 by Auto_tac;
 bind_thm ("while_true_E", refl RSN (2, result() RS mp));
@@ -115,7 +115,7 @@
 
 (** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  WHILE e DO c **)
 
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
 \              (c' = WHILE e DO c) --> \
 \              (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
 by (etac exec.induct 1);
@@ -124,7 +124,7 @@
 bind_thm ("while_if1", refl RSN (2, result() RS mp));
 
 
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
 \              (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
 \              (WHILE e DO c, s) -[eval]-> t";
 by (etac exec.induct 1);
@@ -143,7 +143,7 @@
 (** Equivalence of  (IF e THEN c1 ELSE c2);;c
                and  IF e THEN (c1;;c) ELSE (c2;;c)   **)
 
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
 \              (c' = (IF e THEN c1 ELSE c2);;c) --> \
 \              (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
 by (etac exec.induct 1);
@@ -152,7 +152,7 @@
 bind_thm ("if_semi1", refl RSN (2, result() RS mp));
 
 
-Goal "!!x. (c',s) -[eval]-> t ==> \
+Goal "(c',s) -[eval]-> t ==> \
 \              (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
 \              ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
 by (etac exec.induct 1);
@@ -172,7 +172,7 @@
                and  VALOF c1;;c2 RESULTIS e
  **)
 
-Goal "!!x. (e',s) -|-> (v,s') ==> \
+Goal "(e',s) -|-> (v,s') ==> \
 \              (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
 \              (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
 by (etac eval_induct 1);
@@ -181,7 +181,7 @@
 bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
 
 
-Goal "!!x. (e',s) -|-> (v,s') ==> \
+Goal "(e',s) -|-> (v,s') ==> \
 \              (e' = VALOF c1;;c2 RESULTIS e) --> \
 \              (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
 by (etac eval_induct 1);
@@ -198,7 +198,7 @@
 
 (** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
 
-Goal "!!x. (e',s) -|-> (v,s') ==> \
+Goal "(e',s) -|-> (v,s') ==> \
 \              (e' = VALOF SKIP RESULTIS e) --> \
 \              (e, s) -|-> (v,s')";
 by (etac eval_induct 1);
@@ -206,7 +206,7 @@
 by (Blast_tac 1); 
 bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
 
-Goal "!!x. (e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
+Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
 by (Blast_tac 1);
 qed "valof_skip2";
 
@@ -217,7 +217,7 @@
 
 (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
 
-Goal "!!x. (e',s) -|-> (v,s'') ==> \
+Goal "(e',s) -|-> (v,s'') ==> \
 \              (e' = VALOF x:=e RESULTIS X x) --> \
 \              (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
 by (etac eval_induct 1);
@@ -229,7 +229,7 @@
 bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
 
 
-Goal "!!x. (e,s) -|-> (v,s') ==> \
+Goal "(e,s) -|-> (v,s') ==> \
 \              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
 by (Blast_tac 1);
 qed "valof_assign2";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/LFilter.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -18,19 +18,19 @@
 AddSEs [findRel_LConsE];
 
 
-Goal "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
+Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
 by (etac findRel.induct 1);
 by (Blast_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "findRel_functional";
 
-Goal "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
+Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
 by (etac findRel.induct 1);
 by (Blast_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "findRel_imp_LCons";
 
-Goal "!!p. (LNil,l): findRel p ==> R";
+Goal "(LNil,l): findRel p ==> R";
 by (blast_tac (claset() addEs [findRel.elim]) 1);
 qed "findRel_LNil";
 
@@ -39,7 +39,7 @@
 
 (*** Properties of Domain (findRel p) ***)
 
-Goal "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
+Goal "LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
 by (case_tac "p x" 1);
 by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
 qed "LCons_Domain_findRel";
@@ -73,22 +73,22 @@
 qed "find_LNil";
 Addsimps [find_LNil];
 
-Goalw [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
+Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
 by (blast_tac (claset() addDs [findRel_functional]) 1);
 qed "findRel_imp_find";
 Addsimps [findRel_imp_find];
 
-Goal "!!p. p x ==> find p (LCons x l) = LCons x l";
+Goal "p x ==> find p (LCons x l) = LCons x l";
 by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
 qed "find_LCons_found";
 Addsimps [find_LCons_found];
 
-Goalw [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
+Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
 by (Blast_tac 1);
 qed "diverge_find_LNil";
 Addsimps [diverge_find_LNil];
 
-Goal "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
+Goal "~ (p x) ==> find p (LCons x l) = find p l";
 by (case_tac "LCons x l : Domain(findRel p)" 1);
 by (Asm_full_simp_tac 2);
 by (Clarify_tac 1);
@@ -111,7 +111,7 @@
 qed "lfilter_LNil";
 Addsimps [lfilter_LNil];
 
-Goal "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
+Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (Asm_simp_tac 1);
 qed "diverge_lfilter_LNil";
@@ -119,7 +119,7 @@
 Addsimps [diverge_lfilter_LNil];
 
 
-Goal "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
+Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (Asm_simp_tac 1);
 qed "lfilter_LCons_found";
@@ -127,7 +127,7 @@
   subsumes both*)
 
 
-Goal "!!p. (l, LCons x l') : findRel p \
+Goal "(l, LCons x l') : findRel p \
 \              ==> lfilter p l = LCons x (lfilter p l')";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (Asm_simp_tac 1);
@@ -136,7 +136,7 @@
 Addsimps [findRel_imp_lfilter];
 
 
-Goal "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
+Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
 by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
 by (case_tac "LCons x l : Domain(findRel p)" 1);
 by (Asm_full_simp_tac 2);
@@ -155,7 +155,7 @@
 Addsimps [lfilter_LCons];
 
 
-Goal "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
+Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)";
 by (rtac notI 1);
 by (etac Domain_findRelE 1);
 by (etac rev_mp 1);
@@ -163,7 +163,7 @@
 qed "lfilter_eq_LNil";
 
 
-Goal "!!p. lfilter p l = LCons x l' -->     \
+Goal "lfilter p l = LCons x l' -->     \
 \              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
 by (stac (lfilter_def RS def_llist_corec) 1);
 by (case_tac "l : Domain(findRel p)" 1);
@@ -205,7 +205,7 @@
      lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
  ***)
 
-Goal "!!p. (l,l') : findRel q \
+Goal "(l,l') : findRel q \
 \           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
 by (etac findRel.induct 1);
 by (blast_tac (claset() addIs findRel.intrs) 1);
@@ -214,7 +214,7 @@
 
 val findRel_conj = refl RSN (2, findRel_conj_lemma);
 
-Goal "!!p. (l,l'') : findRel (%x. p x & q x) \
+Goal "(l,l'') : findRel (%x. p x & q x) \
 \              ==> (l, LCons x l') : findRel q --> ~ p x     \
 \                  --> l' : Domain (findRel (%x. p x & q x))";
 by (etac findRel.induct 1);
@@ -222,7 +222,7 @@
 qed_spec_mp "findRel_not_conj_Domain";
 
 
-Goal "!!p. (l,lxx) : findRel q ==> \
+Goal "(l,lxx) : findRel q ==> \
 \            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
 \            --> (l,lz) : findRel (%x. p x & q x)";
 by (etac findRel.induct 1);
@@ -230,7 +230,7 @@
 qed_spec_mp "findRel_conj2";
 
 
-Goal "!!p. (lx,ly) : findRel p \
+Goal "(lx,ly) : findRel p \
 \              ==> ALL l. lx = lfilter q l \
 \                  --> l : Domain (findRel(%x. p x & q x))";
 by (etac findRel.induct 1);
@@ -245,7 +245,7 @@
 qed_spec_mp "findRel_lfilter_Domain_conj";
 
 
-Goal "!!p. (l,l'') : findRel(%x. p x & q x) \
+Goal "(l,l'') : findRel(%x. p x & q x) \
 \              ==> l'' = LCons y l' --> \
 \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
 by (etac findRel.induct 1);
@@ -299,13 +299,13 @@
      lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
  ***)
 
-Goal "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
+Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
 by (etac findRel.induct 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "findRel_lmap_Domain";
 
 
-Goal "!!p. lmap f l = LCons x l' -->     \
+Goal "lmap f l = LCons x l' -->     \
 \              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
 by (stac (lmap_def RS def_llist_corec) 1);
 by (res_inst_tac [("l", "l")] llistE 1);
@@ -313,7 +313,7 @@
 qed_spec_mp "lmap_eq_LCons";
 
 
-Goal "!!p. (lx,ly) : findRel p ==>  \
+Goal "(lx,ly) : findRel p ==>  \
 \    ALL l. lmap f l = lx --> ly = LCons x l' --> \
 \    (EX y l''. x = f y & l' = lmap f l'' &       \
 \    (l, LCons y l'') : findRel(%x. p(f x)))";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -13,7 +13,7 @@
 Addsplits [split_split, split_sum_case];
 
 (*This justifies using llist in other recursive type definitions*)
-Goalw llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
+Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
 by (rtac gfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "llist_mono";
@@ -190,7 +190,7 @@
     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
  **)
 
-Goalw [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
+Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
 by (REPEAT (ares_tac basic_monos 1));
 qed "LListD_Fun_mono";
 
@@ -335,7 +335,7 @@
 
 (*A typical use of co-induction to show membership in the gfp.
   The containing set is simply the singleton {Lconst(M)}. *)
-Goal "!!M A. M:A ==> Lconst(M): llist(A)";
+Goal "M:A ==> Lconst(M): llist(A)";
 by (rtac (singletonI RS llist_coinduct) 1);
 by Safe_tac;
 by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
@@ -522,12 +522,12 @@
           Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
 
 
-Goal "!!M. M: llist(A) ==> Lappend NIL M = M";
+Goal "M: llist(A) ==> Lappend NIL M = M";
 by (etac LList_fun_equalityI 1);
 by (ALLGOALS Asm_simp_tac);
 qed "Lappend_NIL";
 
-Goal "!!M. M: llist(A) ==> Lappend M NIL = M";
+Goal "M: llist(A) ==> Lappend M NIL = M";
 by (etac LList_fun_equalityI 1);
 by (ALLGOALS Asm_simp_tac);
 qed "Lappend_NIL2";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -10,7 +10,7 @@
 
 (** The union of two disjoint tilings is a tiling **)
 
-Goal "!!t. t: tiling A ==> \
+Goal "t: tiling A ==> \
 \              u: tiling A --> t <= Compl u --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (Simp_tac 1);
@@ -101,7 +101,7 @@
 
 (*** Dominoes ***)
 
-Goal "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
+Goal "[| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
 by (eresolve_tac [domino.elim] 1);
 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
 by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
@@ -111,20 +111,20 @@
            THEN Blast_tac 1));
 qed "domino_singleton";
 
-Goal "!!d. d:domino ==> finite d";
+Goal "d:domino ==> finite d";
 by (blast_tac (claset() addSEs [domino.elim]) 1);
 qed "domino_finite";
 
 
 (*** Tilings of dominoes ***)
 
-Goal "!!t. t:tiling domino ==> finite t";
+Goal "t:tiling domino ==> finite t";
 by (eresolve_tac [tiling.induct] 1);
 by (rtac Finites.emptyI 1);
 by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1);
 qed "tiling_domino_finite";
 
-Goal "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
+Goal "t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
 by (eresolve_tac [tiling.induct] 1);
 by (simp_tac (simpset() addsimps [evnodd_def]) 1);
 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
@@ -132,7 +132,7 @@
 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
 by (Clarify_tac 1);
-by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
+by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd t b" 1);
 by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1);
 by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] 
                         addEs  [equalityE]) 1);
@@ -140,7 +140,7 @@
 
 (*Final argument is surprisingly complex.  Note the use of small simpsets
   to avoid moving Sucs, etc.*)
-Goal "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
+Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
 \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
 \                |] ==> t' ~: tiling domino";
 by (rtac notI 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Perm.ML
--- a/src/HOL/Induct/Perm.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Perm.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -22,23 +22,23 @@
 (** Some examples of rule induction on permutations **)
 
 (*The form of the premise lets the induction bind xs and ys.*)
-Goal "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
+Goal "xs <~~> ys ==> xs=[] --> ys=[]";
 by (etac perm.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "perm_Nil_lemma";
 
 (*A more general version is actually easier to understand!*)
-Goal "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
+Goal "xs <~~> ys ==> length(xs) = length(ys)";
 by (etac perm.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "perm_length";
 
-Goal "!!xs. xs <~~> ys ==> ys <~~> xs";
+Goal "xs <~~> ys ==> ys <~~> xs";
 by (etac perm.induct 1);
 by (REPEAT (ares_tac perm.intrs 1));
 qed "perm_sym";
 
-Goal "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
+Goal "[| xs <~~> ys |] ==> x mem xs --> x mem ys";
 by (etac perm.induct 1);
 by (Fast_tac 4);
 by (ALLGOALS Asm_simp_tac);
@@ -84,13 +84,13 @@
 by (etac perm.Cons 1);
 qed "perm_rev";
 
-Goal "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
+Goal "xs <~~> ys ==> l@xs <~~> l@ys";
 by (list.induct_tac "l" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1);
 qed "perm_append1";
 
-Goal "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
+Goal "xs <~~> ys ==> xs@l <~~> ys@l";
 by (rtac (perm_append_swap RS perm.trans) 1);
 by (etac (perm_append1 RS perm.trans) 1);
 by (rtac perm_append_swap 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/PropLog.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -11,7 +11,7 @@
 open PropLog;
 
 (** Monotonicity **)
-Goalw thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
+Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "thms_mono";
@@ -34,12 +34,12 @@
 val weaken_left_Un1  =    Un_upper1 RS weaken_left;
 val weaken_left_Un2  =    Un_upper2 RS weaken_left;
 
-Goal "!!H. H |- q ==> H |- p->q";
+Goal "H |- q ==> H |- p->q";
 by (fast_tac (claset() addIs [thms.K,thms.MP]) 1);
 qed "weaken_right";
 
 (*The deduction theorem*)
-Goal "!!H. insert p H |- q  ==>  H |- p->q";
+Goal "insert p H |- q  ==>  H |- p->q";
 by (etac thms.induct 1);
 by (ALLGOALS 
     (fast_tac (claset() addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
@@ -75,7 +75,7 @@
 Addsimps [eval_false, eval_var, eval_imp];
 
 (*Soundness of the rules wrt truth-table semantics*)
-Goalw [sat_def] "!!H. H |- p ==> H |= p";
+Goalw [sat_def] "H |- p ==> H |= p";
 by (etac thms.induct 1);
 by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5);
 by (ALLGOALS Asm_simp_tac);
@@ -83,7 +83,7 @@
 
 (*** Towards the completeness proof ***)
 
-Goal "!!H. H |- p->false ==> H |- p->q";
+Goal "H |- p->false ==> H |- p->q";
 by (rtac deduction 1);
 by (etac (weaken_left_insert RS thms_notE) 1);
 by (rtac thms.H 1);
@@ -206,12 +206,12 @@
 qed "completeness_0";
 
 (*A semantic analogue of the Deduction Theorem*)
-Goalw [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
+Goalw [sat_def] "insert p H |= q ==> H |= p->q";
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "sat_imp";
 
-Goal "!!H. finite H ==> !p. H |= p --> H |- p";
+Goal "finite H ==> !p. H |= p --> H |- p";
 by (etac finite_induct 1);
 by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0]));
 by (rtac (weaken_left_insert RS thms.MP) 1);
@@ -221,6 +221,6 @@
 
 val completeness = completeness_lemma RS spec RS mp;
 
-Goal "!!H. finite H ==> (H |- p) = (H |= p)";
+Goal "finite H ==> (H |- p) = (H |= p)";
 by (fast_tac (claset() addSEs [soundness, completeness]) 1);
 qed "syntax_iff_semantics";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/SList.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -18,7 +18,7 @@
 qed "list_unfold";
 
 (*This justifies using list in other recursive type definitions*)
-Goalw list.defs "!!A B. A<=B ==> list(A) <= list(B)";
+Goalw list.defs "A<=B ==> list(A) <= list(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "list_mono";
@@ -113,7 +113,7 @@
 
 AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
 
-Goal "!!N. N: list(A) ==> !M. N ~= CONS M N";
+Goal "N: list(A) ==> !M. N ~= CONS M N";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "not_CONS_self";
@@ -191,7 +191,7 @@
 by (Simp_tac 1);
 qed "List_rec_NIL";
 
-Goal "!!M. [| M: sexp;  N: sexp |] ==> \
+Goal "[| M: sexp;  N: sexp |] ==> \
 \    List_rec (CONS M N) c h = h M N (List_rec N c h)";
 by (rtac (List_rec_unfold RS trans) 1);
 by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
@@ -246,9 +246,9 @@
 by (rtac list_rec_Cons 1);
 qed "Rep_map_Cons";
 
-Goalw [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
+val prems = Goalw [Rep_map_def] "(!!x. f(x): A) ==> Rep_map f xs: list(A)";
 by (rtac list_induct2 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
 qed "Rep_map_type";
 
 Goalw [Abs_map_def] "Abs_map g NIL = Nil";
@@ -366,11 +366,12 @@
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose2";
 
-Goal "!!f. (!!x. f(x): sexp) ==> \
+val prems = 
+Goal "(!!x. f(x): sexp) ==> \
 \       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
 by (list_ind_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac(simpset() addsimps
-			   [Rep_map_type, list_sexp RS subsetD])));
+			   (prems@[Rep_map_type, list_sexp RS subsetD]))));
 qed "Abs_Rep_map";
 
 Addsimps [append_Nil4, map_ident2];
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Simult.ML
--- a/src/HOL/Induct/Simult.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Simult.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -23,7 +23,7 @@
 
 val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
 
-Goalw [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
+Goalw [TF_def] "A<=B ==> TF(A) <= TF(B)";
 by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
 qed "TF_mono";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Induct/Term.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -17,7 +17,7 @@
 qed "term_unfold";
 
 (*This justifies using term in other recursive type definitions*)
-Goalw term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+Goalw term.defs "A<=B ==> term(A) <= term(B)";
 by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
 qed "term_mono";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Integ/Equiv.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -49,7 +49,7 @@
 by (Blast_tac 1);
 qed "equiv_class_subset";
 
-Goal "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
+Goal "[| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
 by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
 by (rewrite_goals_tac [equiv_def,sym_def]);
 by (Blast_tac 1);
@@ -98,7 +98,7 @@
 
 (** Introduction/elimination rules -- needed? **)
 
-Goalw [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
+Goalw [quotient_def] "x:A ==> r^^{x}: A/r";
 by (Blast_tac 1);
 qed "quotientI";
 
@@ -139,7 +139,7 @@
 **)
 
 (*Conversion rule*)
-Goal "!!A r. [| equiv A r;  congruent r b;  a: A |] \
+Goal "[| equiv A r;  congruent r b;  a: A |] \
 \                      ==> (UN x:r^^{a}. b(x)) = b(a)";
 by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
@@ -244,7 +244,7 @@
 (*** Cardinality results suggested by Florian Kammueller ***)
 
 (*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
-Goal "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
+Goal "[| finite A; r <= A Times A |] ==> finite (A/r)";
 by (rtac finite_subset 1);
 by (etac (finite_Pow_iff RS iffD2) 2);
 by (rewtac quotient_def);
@@ -258,7 +258,7 @@
 by (Blast_tac 1);
 qed "finite_equiv_class";
 
-Goal "!!A. [| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] \
+Goal "[| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] \
 \              ==> k dvd card(A)";
 by (rtac (Union_quotient RS subst) 1);
 by (assume_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -568,7 +568,7 @@
 by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
 qed "zless_zadd_Suc";
 
-Goal "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
+Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (simp_tac 
     (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
@@ -598,7 +598,7 @@
 (* z<z ==> R *)
 bind_thm ("zless_irrefl", (zless_not_refl RS notE));
 
-Goal "!!w. z<w ==> w ~= (z::int)";
+Goal "z<w ==> w ~= (z::int)";
 by (fast_tac (claset() addEs [zless_irrefl]) 1);
 qed "zless_not_refl2";
 
@@ -629,30 +629,30 @@
 by (simp_tac (simpset() addsimps [zless_eq_less]) 1);
 qed "zle_eq_le";
 
-Goalw [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
+Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
 by (assume_tac 1);
 qed "zleI";
 
-Goalw [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
+Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
 by (assume_tac 1);
 qed "zleD";
 
 val zleE = make_elim zleD;
 
-Goalw [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
+Goalw [zle_def] "~ z <= w ==> w<(z::int)";
 by (Fast_tac 1);
 qed "not_zleE";
 
-Goalw [zle_def] "!!z. z < w ==> z <= (w::int)";
+Goalw [zle_def] "z < w ==> z <= (w::int)";
 by (fast_tac (claset() addEs [zless_asym]) 1);
 qed "zless_imp_zle";
 
-Goalw [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
+Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
 qed "zle_imp_zless_or_eq";
 
-Goalw [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
+Goalw [zle_def] "z<w | z=w ==> z <=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
 qed "zless_or_eq_imp_zle";
@@ -670,12 +670,12 @@
 by (fast_tac (claset() addIs [zless_trans]) 1);
 qed "zle_zless_trans";
 
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
             rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
 qed "zle_trans";
 
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
+Goal "[| z <= w; w <= z |] ==> z = (w::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
             fast_tac (claset() addEs [zless_irrefl,zless_asym])]);
 qed "zle_anti_sym";
@@ -736,7 +736,7 @@
 Addsimps [zless_eq_less, zle_eq_le,
 	  znegative_zminus_znat, not_znegative_znat]; 
 
-Goal "!! x. (x::int) = y ==> x <= y"; 
+Goal "(x::int) = y ==> x <= y"; 
   by (etac subst 1); by (rtac zle_refl 1); 
 qed "zequalD1"; 
 
@@ -822,16 +822,16 @@
 Addsimps [zminus_zless_zminus, zminus_zle_zminus, 
 	  negative_eq_positive, not_znat_zless_negative]; 
 
-Goalw [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
+Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
   by Auto_tac; 
 qed "znegative_less_0"; 
 
-Goalw [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
+Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)";
   by (stac znegative_less_0 1); 
   by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); 
 qed "not_znegative_ge_0"; 
 
-Goal "!! x. znegative x ==> ? n. x = $~ $# Suc n"; 
+Goal "znegative x ==> ? n. x = $~ $# Suc n"; 
   by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); 
   by (etac exE 1); 
   by (rtac exI 1);
@@ -839,7 +839,7 @@
   by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); 
 qed "znegativeD"; 
 
-Goal "!! x. ~znegative x ==> ? n. x = $# n"; 
+Goal "~znegative x ==> ? n. x = $# n"; 
   by (dtac (not_znegative_ge_0 RS iffD1) 1); 
   by (dtac zle_imp_zless_or_eq 1); 
   by (etac disjE 1); 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Map.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -108,7 +108,7 @@
 qed "ran_empty";
 Addsimps [ran_empty];
 
-Goalw [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)";
+Goalw [ran_def] "m a = None ==> ran(m[a|->b]) = insert b (ran m)";
 by Auto_tac;
 by (subgoal_tac "~(aa = a)" 1);
 by Auto_tac;
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/NatDef.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -130,7 +130,7 @@
 
 bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
 
-Goal "!!n. n ~= 0 ==> EX m. n = Suc m";
+Goal "n ~= 0 ==> EX m. n = Suc m";
 by (rtac natE 1);
 by (REPEAT (Blast_tac 1));
 qed "not0_implies_Suc";
@@ -246,7 +246,7 @@
 (* n<n ==> R *)
 bind_thm ("less_irrefl", (less_not_refl RS notE));
 
-Goal "!!m. n<m ==> m ~= (n::nat)";
+Goal "n<m ==> m ~= (n::nat)";
 by (blast_tac (claset() addSEs [less_irrefl]) 1);
 qed "less_not_refl2";
 
@@ -313,14 +313,14 @@
 qed "not_gr0";
 Addsimps [not_gr0];
 
-Goal "!!m. m<n ==> 0 < n";
+Goal "m<n ==> 0 < n";
 by (dtac gr_implies_not0 1);
 by (Asm_full_simp_tac 1);
 qed "gr_implies_gr0";
 Addsimps [gr_implies_gr0];
 
 
-Goal "!!m n. m<n ==> Suc(m) < Suc(n)";
+Goal "m<n ==> Suc(m) < Suc(n)";
 by (etac rev_mp 1);
 by (nat_ind_tac "n" 1);
 by (ALLGOALS (fast_tac (claset() addEs  [less_trans, lessE])));
@@ -354,7 +354,7 @@
 
 (** Inductive (?) properties **)
 
-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() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
 qed "Suc_lessI";
@@ -375,7 +375,7 @@
 by (assume_tac 1);
 qed "Suc_lessE";
 
-Goal "!!m n. Suc(m) < Suc(n) ==> m<n";
+Goal "Suc(m) < Suc(n) ==> m<n";
 by (blast_tac (claset() addEs [lessE, make_elim Suc_lessD]) 1);
 qed "Suc_less_SucD";
 
@@ -390,7 +390,7 @@
 qed "not_Suc_n_less_n";
 Addsimps [not_Suc_n_less_n];
 
-Goal "!!i. i<j ==> j<k --> Suc i < k";
+Goal "i<j ==> j<k --> Suc i < k";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (simpset())));
 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
@@ -456,7 +456,7 @@
           n_not_Suc_n, Suc_n_not_n,
           nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
 
-Goal "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)";
+Goal "(m <= Suc(n)) = (m<=n | m = Suc n)";
 by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
 qed "le_Suc_eq";
@@ -501,7 +501,7 @@
 by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
 qed "not_less_iff_le";
 
-Goalw [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
+Goalw [le_def] "~ m <= n ==> n<(m::nat)";
 by (Blast_tac 1);
 qed "not_leE";
 
@@ -509,12 +509,12 @@
 by (Simp_tac 1);
 qed "not_le_iff_less";
 
-Goalw [le_def] "!!m. m < n ==> Suc(m) <= n";
+Goalw [le_def] "m < n ==> Suc(m) <= n";
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
 by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1);
 qed "Suc_leI";  (*formerly called lessD*)
 
-Goalw [le_def] "!!m. Suc(m) <= n ==> m <= n";
+Goalw [le_def] "Suc(m) <= n ==> m <= n";
 by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
 qed "Suc_leD";
 
@@ -530,25 +530,25 @@
 by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1);
 qed "Suc_le_eq";
 
-Goalw [le_def] "!!m. m <= n ==> m <= Suc n";
+Goalw [le_def] "m <= n ==> m <= Suc n";
 by (blast_tac (claset() addDs [Suc_lessD]) 1);
 qed "le_SucI";
 Addsimps[le_SucI];
 
 bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
 
-Goalw [le_def] "!!m. m < n ==> m <= (n::nat)";
+Goalw [le_def] "m < n ==> m <= (n::nat)";
 by (blast_tac (claset() addEs [less_asym]) 1);
 qed "less_imp_le";
 
 (** Equivalence of m<=n and  m<n | m=n **)
 
-Goalw [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
+Goalw [le_def] "m <= n ==> m < n | m=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1);
 qed "le_imp_less_or_eq";
 
-Goalw [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
+Goalw [le_def] "m<n | m=n ==> m <=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1);
 qed "less_or_eq_imp_le";
@@ -564,22 +564,22 @@
 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 qed "le_refl";
 
-Goal "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
+Goal "[| i <= j; j < k |] ==> i < (k::nat)";
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]
 	                addIs [less_trans]) 1);
 qed "le_less_trans";
 
-Goal "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
+Goal "[| i < j; j <= k |] ==> i < (k::nat)";
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]
 	                addIs [less_trans]) 1);
 qed "less_le_trans";
 
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::nat)";
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]
 	                addIs [less_or_eq_imp_le, less_trans]) 1);
 qed "le_trans";
 
-Goal "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
+Goal "[| m <= n; n <= m |] ==> m = (n::nat)";
 (*order_less_irrefl could make this proof fail*)
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]
 	                addSEs [less_irrefl] addEs [less_asym]) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Ord.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -42,8 +42,8 @@
 
 (** min **)
 
-Goalw [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
-by (Asm_simp_tac 1);
+val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
+by (simp_tac (simpset() addsimps prems) 1);
 qed "min_leastL";
 
 val prems = goalw thy [min_def]
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Power.ML
--- a/src/HOL/Power.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Power.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -22,7 +22,7 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
 qed "power_mult";
 
-Goal "!! i. 0 < i ==> 0 < i^n";
+Goal "0 < i ==> 0 < i^n";
 by (induct_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
 qed "zero_less_power";
@@ -33,14 +33,14 @@
 by (Blast_tac 1);
 qed "le_imp_power_dvd";
 
-Goal "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
+Goal "[| 0 < i; i^m < i^n |] ==> m<n";
 by (rtac ccontr 1);
 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
 by (etac zero_less_power 1);
 by (contr_tac 1);
 qed "power_less_imp_less";
 
-Goal "!!n. k^j dvd n --> i<j --> k^i dvd n";
+Goal "k^j dvd n --> i<j --> k^i dvd n";
 by (induct_tac "j" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
 by (stac mult_commute 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Prod.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -189,7 +189,7 @@
 by (Asm_simp_tac 1);
 qed "splitI2";
 
-Goal "!!a b c. c a b ==> split c (a,b)";
+Goal "c a b ==> split c (a,b)";
 by (Asm_simp_tac 1);
 qed "splitI";
 
@@ -204,11 +204,11 @@
 	rtac (split_beta RS subst) 1,
 	rtac (hd prems) 1]);
 
-Goal "!!R a b. split R (a,b) ==> R a b";
+Goal "split R (a,b) ==> R a b";
 by (etac (split RS iffD1) 1);
 qed "splitD";
 
-Goal "!!a b c. z: c a b ==> z: split c (a,b)";
+Goal "z: c a b ==> z: split c (a,b)";
 by (Asm_simp_tac 1);
 qed "mem_splitI";
 
@@ -241,7 +241,7 @@
 but cannot be used as rewrite rule:
 ### Cannot add premise as rewrite rule because it contains (type) unknowns:
 ### ?y = .x
-Goal "!!P. [| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
+Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
 by (rtac select_equality 1);
 by ( Simp_tac 1);
 by (split_all_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/Lubs.ML
--- a/src/HOL/Real/Lubs.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/Lubs.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -10,34 +10,34 @@
 (*------------------------------------------------------------------------
                         Rules for *<= and <=*
  ------------------------------------------------------------------------*)
-Goalw [setle_def] "!!x. ALL y: S. y <= x ==> S *<= x";
+Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x";
 by (assume_tac 1);
 qed "setleI";
 
-Goalw [setle_def] "!!x. [| S *<= x; y: S |] ==> y <= x";
+Goalw [setle_def] "[| S *<= x; y: S |] ==> y <= x";
 by (Fast_tac 1);
 qed "setleD";
 
-Goalw [setge_def] "!!x. ALL y: S. x<= y ==> x <=* S";
+Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S";
 by (assume_tac 1);
 qed "setgeI";
 
-Goalw [setge_def] "!!x. [| x <=* S; y: S |] ==> x <= y";
+Goalw [setge_def] "[| x <=* S; y: S |] ==> x <= y";
 by (Fast_tac 1);
 qed "setgeD";
 
 (*------------------------------------------------------------------------
                         Rules about leastP, ub and lub
  ------------------------------------------------------------------------*)
-Goalw [leastP_def] "!!x. leastP P x ==> P x";
+Goalw [leastP_def] "leastP P x ==> P x";
 by (Step_tac 1);
 qed "leastPD1";
 
-Goalw [leastP_def] "!!x. leastP P x ==> x <=* Collect P";
+Goalw [leastP_def] "leastP P x ==> x <=* Collect P";
 by (Step_tac 1);
 qed "leastPD2";
 
-Goal "!!x. [| leastP P x; y: Collect P |] ==> x <= y";
+Goal "[| leastP P x; y: Collect P |] ==> x <= y";
 by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1);
 qed "leastPD3";
 
@@ -51,19 +51,19 @@
 by (Step_tac 1);
 qed "isLubD1a";
 
-Goalw [isUb_def] "!!x. isLub R S x ==> isUb R S x";
+Goalw [isUb_def] "isLub R S x ==> isUb R S x";
 by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1);
 qed "isLub_isUb";
 
-Goal "!!x. [| isLub R S x; y : S |] ==> y <= x";
+Goal "[| isLub R S x; y : S |] ==> y <= x";
 by (blast_tac (claset() addSDs [isLubD1,setleD]) 1);
 qed "isLubD2";
 
-Goalw [isLub_def] "!!x. isLub R S x ==> leastP(isUb R S) x";
+Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x";
 by (assume_tac 1);
 qed "isLubD3";
 
-Goalw [isLub_def] "!!x. leastP(isUb R S) x ==> isLub R S x";
+Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x";
 by (assume_tac 1);
 qed "isLubI1";
 
@@ -72,27 +72,27 @@
 by (Step_tac 1);
 qed "isLubI2";
 
-Goalw [isUb_def] "!!x. [| isUb R S x; y : S |] ==> y <= x";
+Goalw [isUb_def] "[| isUb R S x; y : S |] ==> y <= x";
 by (fast_tac (claset() addDs [setleD]) 1);
 qed "isUbD";
 
-Goalw [isUb_def] "!!x. isUb R S x ==> S *<= x";
+Goalw [isUb_def] "isUb R S x ==> S *<= x";
 by (Step_tac 1);
 qed "isUbD2";
 
-Goalw [isUb_def] "!!x. isUb R S x ==> x: R";
+Goalw [isUb_def] "isUb R S x ==> x: R";
 by (Step_tac 1);
 qed "isUbD2a";
 
-Goalw [isUb_def] "!!x. [| S *<= x; x: R |] ==> isUb R S x";
+Goalw [isUb_def] "[| S *<= x; x: R |] ==> isUb R S x";
 by (Step_tac 1);
 qed "isUbI";
 
-Goalw [isLub_def] "!!x. [| isLub R S x; isUb R S y |] ==> x <= y";
+Goalw [isLub_def] "[| isLub R S x; isUb R S y |] ==> x <= y";
 by (blast_tac (claset() addSIs [leastPD3]) 1);
 qed "isLub_le_isUb";
 
-Goalw [ubs_def,isLub_def] "!!x. isLub R S x ==> x <=* ubs R S";
+Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S";
 by (etac leastPD2 1);
 qed "isLub_ubs";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/PNat.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -102,12 +102,12 @@
 
 Addsimps [zero_not_mem_pnat];
 
-Goal "!!x. x : pnat ==> 0 < x";
+Goal "x : pnat ==> 0 < x";
 by (dtac (pnat_unfold RS subst) 1);
 by Auto_tac;
 qed "mem_pnat_gt_zero";
 
-Goal "!!x. 0 < x ==> x: pnat";
+Goal "0 < x ==> x: pnat";
 by (stac pnat_unfold 1);
 by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); 
 by (etac exE 1 THEN Asm_simp_tac 1);
@@ -177,7 +177,7 @@
 
 bind_thm ("pSuc_n_not_n", n_not_pSuc_n RS not_sym);
 
-Goal "!!n. n ~= 1p ==> EX m. n = pSuc m";
+Goal "n ~= 1p ==> EX m. n = pSuc m";
 by (rtac pnatE 1);
 by (REPEAT (Blast_tac 1));
 qed "not1p_implies_pSuc";
@@ -245,14 +245,14 @@
 by ((etac less_trans 1) THEN assume_tac 1);
 qed "pnat_less_trans";
 
-Goalw [pnat_less_def] "!!x. x < (y::pnat) ==> ~ y < x";
+Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
 by (etac less_not_sym 1);
 qed "pnat_less_not_sym";
 
 (* [| x < y; y < x |] ==> P *)
 bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE);
 
-Goalw [pnat_less_def] "!!x. ~ y < (y::pnat)";
+Goalw [pnat_less_def] "~ y < (y::pnat)";
 by Auto_tac;
 qed "pnat_less_not_refl";
 
@@ -304,11 +304,11 @@
 
    (*** pnat_le ***)
 
-Goalw [pnat_le_def] "!!x. ~ (x::pnat) < y ==> y <= x";
+Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x";
 by (assume_tac 1);
 qed "pnat_leI";
 
-Goalw [pnat_le_def] "!!x. (x::pnat) <= y ==> ~ y < x";
+Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
 by (assume_tac 1);
 qed "pnat_leD";
 
@@ -318,22 +318,22 @@
 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
 qed "pnat_not_less_iff_le";
 
-Goalw [pnat_le_def] "!!x. ~(x::pnat) <= y ==> y < x";
+Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x";
 by (Blast_tac 1);
 qed "pnat_not_leE";
 
-Goalw [pnat_le_def] "!!x. (x::pnat) < y ==> x <= y";
+Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y";
 by (blast_tac (claset() addEs [pnat_less_asym]) 1);
 qed "pnat_less_imp_le";
 
 (** Equivalence of m<=n and  m<n | m=n **)
 
-Goalw [pnat_le_def] "!!m. m <= n ==> m < n | m=(n::pnat)";
+Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)";
 by (cut_facts_tac [pnat_less_linear] 1);
 by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1);
 qed "pnat_le_imp_less_or_eq";
 
-Goalw [pnat_le_def] "!!m. m<n | m=n ==> m <=(n::pnat)";
+Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)";
 by (cut_facts_tac [pnat_less_linear] 1);
 by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1);
 qed "pnat_less_or_eq_imp_le";
@@ -351,19 +351,19 @@
 by (blast_tac (claset() addIs [pnat_less_trans]) 1);
 qed "pnat_le_less_trans";
 
-Goal "!!i. [| i < j; j <= k |] ==> i < (k::pnat)";
+Goal "[| i < j; j <= k |] ==> i < (k::pnat)";
 by (dtac pnat_le_imp_less_or_eq 1);
 by (blast_tac (claset() addIs [pnat_less_trans]) 1);
 qed "pnat_less_le_trans";
 
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::pnat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)";
 by (EVERY1[dtac pnat_le_imp_less_or_eq, 
            dtac pnat_le_imp_less_or_eq,
            rtac pnat_less_or_eq_imp_le, 
            blast_tac (claset() addIs [pnat_less_trans])]);
 qed "pnat_le_trans";
 
-Goal "!!m. [| m <= n; n <= m |] ==> m = (n::pnat)";
+Goal "[| m <= n; n <= m |] ==> m = (n::pnat)";
 by (EVERY1[dtac pnat_le_imp_less_or_eq, 
            dtac pnat_le_imp_less_or_eq,
            blast_tac (claset() addIs [pnat_less_asym])]);
@@ -440,7 +440,7 @@
 (*"i < j ==> i < m + j"*)
 bind_thm ("pnat_trans_less_add2", pnat_le_add2 RSN (2,pnat_less_le_trans));
 
-Goalw [pnat_less_def] "!!i. i+j < (k::pnat) ==> i<k";
+Goalw [pnat_less_def] "i+j < (k::pnat) ==> i<k";
 by (auto_tac (claset() addEs [add_lessD1],
     simpset() addsimps [sum_Rep_pnat_sum RS sym]));
 qed "pnat_add_lessD1";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/PRat.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -302,7 +302,7 @@
     prat_mult_1,prat_mult_1_right]) 1);
 qed "prat_qinv_left_ex1";
 
-Goal "!!y. x * y = $# Abs_pnat 1 ==> x = qinv y";
+Goal "x * y = $# Abs_pnat 1 ==> x = qinv y";
 by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
 by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
 by (Blast_tac 1);
@@ -580,32 +580,32 @@
 by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
 qed "prat_self_less_add_left";
 
-Goalw [prat_less_def] "!!y. $#1p < y ==> (x::prat) < x * y";
+Goalw [prat_less_def] "$#1p < y ==> (x::prat) < x * y";
 by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
     prat_add_mult_distrib2]));
 qed "prat_self_less_mult_right";
 
 (*** Properties of <= ***)
 
-Goalw [prat_le_def] "!!w. ~(w < z) ==> z <= (w::prat)";
+Goalw [prat_le_def] "~(w < z) ==> z <= (w::prat)";
 by (assume_tac 1);
 qed "prat_leI";
 
-Goalw [prat_le_def] "!!w. z<=w ==> ~(w<(z::prat))";
+Goalw [prat_le_def] "z<=w ==> ~(w<(z::prat))";
 by (assume_tac 1);
 qed "prat_leD";
 
 val prat_leE = make_elim prat_leD;
 
-Goal "!!w. (~(w < z)) = (z <= (w::prat))";
+Goal "(~(w < z)) = (z <= (w::prat))";
 by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
 qed "prat_less_le_iff";
 
-Goalw [prat_le_def] "!!z. ~ z <= w ==> w<(z::prat)";
+Goalw [prat_le_def] "~ z <= w ==> w<(z::prat)";
 by (Fast_tac 1);
 qed "not_prat_leE";
 
-Goalw [prat_le_def] "!!z. z < w ==> z <= (w::prat)";
+Goalw [prat_le_def] "z < w ==> z <= (w::prat)";
 by (fast_tac (claset() addEs [prat_less_asym]) 1);
 qed "prat_less_imp_le";
 
@@ -614,7 +614,7 @@
 by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
 qed "prat_le_imp_less_or_eq";
 
-Goalw [prat_le_def] "!!z. z<w | z=w ==> z <=(w::prat)";
+Goalw [prat_le_def] "z<w | z=w ==> z <=(w::prat)";
 by (cut_facts_tac [prat_linear] 1);
 by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
 qed "prat_less_or_eq_imp_le";
@@ -637,17 +637,17 @@
 by (fast_tac (claset() addIs [prat_less_trans]) 1);
 qed "prat_less_le_trans";
 
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::prat)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
 by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
             rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
 qed "prat_le_trans";
 
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::prat)";
+Goal "[| z <= w; w <= z |] ==> z = (w::prat)";
 by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
             fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
 qed "prat_le_anti_sym";
 
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::prat)";
+Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
 by (rtac not_prat_leE 1);
 by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
 qed "not_less_not_eq_prat_less";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/PReal.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -35,7 +35,7 @@
 
 Addsimps [one_set_mem_preal];
 
-Goalw [preal_def] "!!x. x : preal ==> {} < x";
+Goalw [preal_def] "x : preal ==> {} < x";
 by (Fast_tac 1);
 qed "preal_psubset_empty";
 
@@ -188,7 +188,7 @@
 (* A positive fraction not in a positive real is an upper bound *)
 (* Gleason p. 122 - Remark (1)                                  *)
 
-Goal "!!x. x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
+Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
 by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
 by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
 qed "not_in_preal_ub";
@@ -488,40 +488,40 @@
               simpset() addsimps [prat_add_mult_distrib2]));
 qed "lemma_prat_add_mult_mono";
 
-Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
+Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
 \                  Rep_preal w; yb: Rep_preal w |] ==> \
 \                  xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
 by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
 qed "lemma_add_mult_mem_Rep_preal";
 
-Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
+Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
 \                  Rep_preal w; yb: Rep_preal w |] ==> \
 \                  yb*(xb + xc): Rep_preal (w*(z1 + z2))";
 by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
 qed "lemma_add_mult_mem_Rep_preal1";
 
-Goal "!!x. x: Rep_preal (w * z1 + w * z2) ==> \
+Goal "x: Rep_preal (w * z1 + w * z2) ==> \
 \              x: Rep_preal (w * (z1 + z2))";
 by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
               simpset()));
-by (forw_inst_tac [("ya","xb"),("yb","xc"),("xb","ya"),("xc","yb")] 
+by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")] 
                                    lemma_add_mult_mem_Rep_preal1 1);
 by Auto_tac;
-by (res_inst_tac [("q1.0","xb"),("q2.0","xc")] prat_linear_less2 1);
+by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1);
 by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
 by (rtac (Rep_preal RS prealE_lemma3b) 1);
 by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
-by (dres_inst_tac [("ya","xc"),("yb","xb"),("xc","ya"),("xb","yb")] 
+by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")] 
                                    lemma_add_mult_mem_Rep_preal1 1);
 by Auto_tac;
 by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
 by (rtac (Rep_preal RS prealE_lemma3b) 1);
-by (thin_tac "xc * ya + xc * yb  : Rep_preal (w * (z1 + z2))" 1);
+by (thin_tac "xb * ya + xb * yb  : Rep_preal (w * (z1 + z2))" 1);
 by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
               prat_add_commute] @ preal_add_ac ));
 qed "lemma_preal_add_mult_distrib";
 
-Goal "!!x. x: Rep_preal (w * (z1 + z2)) ==> \
+Goal "x: Rep_preal (w * (z1 + z2)) ==> \
 \              x: Rep_preal (w * z1 + w * z2)";
 by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
               addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
@@ -610,7 +610,7 @@
 qed "preal_mem_inv_set";
 
 (*more lemmas for inverse *)
-Goal "!!x. x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
+Goal "x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
 by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
               simpset() addsimps [pinv_def,preal_prat_def] ));
 by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
@@ -620,7 +620,7 @@
 qed "preal_mem_mult_invD";
 
 (*** Gleason's Lemma 9-3.4 p 122 ***)
-Goal "!!p. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
+Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
 \            ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
 by (cut_facts_tac [mem_Rep_preal_Ex] 1);
 by (res_inst_tac [("n","p")] pnat_induct 1);
@@ -637,7 +637,7 @@
     simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
 qed "lemma1b_gleason9_34";
 
-Goal "!!A. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
+Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
 by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
 by (etac exE 1);
 by (dtac not_in_preal_ub 1);
@@ -673,7 +673,7 @@
 (******)
 
 (*** FIXME: long! ***)
-Goal "!!A. $#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "$#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
 by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
 by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
 by (Fast_tac 1);
@@ -696,13 +696,13 @@
 by Auto_tac;
 qed "lemma_gleason9_36";
 
-Goal "!!A. $#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
+Goal "$#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
 by (rtac lemma_gleason9_36 1);
 by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
 qed "lemma_gleason9_36a";
 
 (*** Part 2 of existence of inverse ***)
-Goal "!!x. x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
+Goal "x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
 by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
               simpset() addsimps [pinv_def,preal_prat_def] ));
 by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
@@ -786,11 +786,11 @@
 by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));
 qed "not_preal_leE";
 		       
-Goal "!!w. ~(w < z) ==> z <= (w::preal)";
+Goal "~(w < z) ==> z <= (w::preal)";
 by (fast_tac (claset() addIs [not_preal_leE]) 1);
 qed "preal_leI";
 
-Goal "!!w. (~(w < z)) = (z <= (w::preal))";
+Goal "(~(w < z)) = (z <= (w::preal))";
 by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
 qed "preal_less_le_iff";
 
@@ -827,17 +827,17 @@
 by (fast_tac (claset() addIs [preal_less_trans]) 1);
 qed "preal_less_le_trans";
 
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::preal)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
 by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
             rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
 qed "preal_le_trans";
 
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::preal)";
+Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
 by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
             fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
 qed "preal_le_anti_sym";
 
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::preal)";
+Goal "[| ~ y < x; y ~= x |] ==> x < (y::preal)";
 by (rtac not_preal_leE 1);
 by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
 qed "not_less_not_eq_preal_less";
@@ -849,7 +849,7 @@
 (**** Define the D required and show that it is a positive real ****)
 
 (* useful lemmas - proved elsewhere? *)
-Goalw [psubset_def] "!!A. A < B ==> ? x. x ~: A & x : B";
+Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
 by (etac conjE 1);
 by (etac swap 1);
 by (etac equalityI 1);
@@ -911,7 +911,7 @@
 qed "preal_less_set_not_prat_set";
 
 (** Part 3 of Dedekind sections def **)
-Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
+Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  \      !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
 by Auto_tac;
 by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
@@ -919,7 +919,7 @@
 by Auto_tac;
 qed "preal_less_set_lemma3";
 
-Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
+Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
 \       Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
 by Auto_tac;
 by (dtac (Rep_preal RS prealE_lemma4a) 1);
@@ -954,7 +954,7 @@
 
 (** proving that B <= A + D  --- trickier **)
 (** lemma **)
-Goal "!!x. x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
+Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
 by (dtac (Rep_preal RS prealE_lemma4a) 1);
 by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
 qed "lemma_sum_mem_Rep_preal_ex";
@@ -1115,7 +1115,7 @@
 (*** Completeness of preal ***)
 
 (*** prove that supremum is a cut ***)
-Goal "!!P. ? (X::preal). X: P ==> \
+Goal "? (X::preal). X: P ==> \
 \         ? q.  q: {w. ? X. X : P & w : Rep_preal X}";
 by Safe_tac;
 by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
@@ -1123,14 +1123,14 @@
 qed "preal_sup_mem_Ex";
 
 (** Part 1 of Dedekind def **)
-Goal "!!P. ? (X::preal). X: P ==> \
+Goal "? (X::preal). X: P ==> \
 \         {} < {w. ? X : P. w : Rep_preal X}";
 by (dtac preal_sup_mem_Ex 1);
 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
 qed "preal_sup_set_not_empty";
 
 (** Part 2 of Dedekind sections def **) 
-Goalw [preal_less_def] "!!P. ? Y. (! X: P. X < Y)  \             
+Goalw [preal_less_def] "? Y. (! X: P. X < Y)  \             
 \         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
 by (auto_tac (claset(),simpset() addsimps [psubset_def]));
 by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
@@ -1139,7 +1139,7 @@
 by (auto_tac (claset() addSDs [bspec],simpset()));
 qed "preal_sup_not_mem_Ex";
 
-Goalw [preal_le_def] "!!P. ? Y. (! X: P. X <= Y)  \
+Goalw [preal_le_def] "? Y. (! X: P. X <= Y)  \
 \         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
 by (Step_tac 1);
 by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
@@ -1148,7 +1148,7 @@
 by (auto_tac (claset() addSDs [bspec],simpset()));
 qed "preal_sup_not_mem_Ex1";
 
-Goal "!!P. ? Y. (! X: P. X < Y)  \                                    
+Goal "? Y. (! X: P. X < Y)  \                                    
 \         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";       (**)
 by (dtac preal_sup_not_mem_Ex 1);
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
@@ -1156,7 +1156,7 @@
 by Auto_tac;
 qed "preal_sup_set_not_prat_set";
 
-Goal "!!P. ? Y. (! X: P. X <= Y)  \
+Goal "? Y. (! X: P. X <= Y)  \
 \         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
 by (dtac preal_sup_not_mem_Ex1 1);
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
@@ -1165,31 +1165,31 @@
 qed "preal_sup_set_not_prat_set1";
 
 (** Part 3 of Dedekind sections def **)
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
 \         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
 \             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";         (**)
 by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
 qed "preal_sup_set_lemma3";
 
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
 \         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
 \             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
 by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
 qed "preal_sup_set_lemma3_1";
 
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
 \         ==>  !y: {w. ? X: P. w: Rep_preal X}. \                        
 \             Bex {w. ? X: P. w: Rep_preal X} (op < y)";                (**)
 by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
 qed "preal_sup_set_lemma4";
 
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
 \         ==>  !y: {w. ? X: P. w: Rep_preal X}. \
 \             Bex {w. ? X: P. w: Rep_preal X} (op < y)";
 by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
 qed "preal_sup_set_lemma4_1";
 
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
 \         ==> {w. ? X: P. w: Rep_preal(X)}: preal";                      (**)
 by (rtac prealI2 1);
 by (rtac preal_sup_set_not_empty 1);
@@ -1199,7 +1199,7 @@
 by Auto_tac;
 qed "preal_sup";
 
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
 \         ==> {w. ? X: P. w: Rep_preal(X)}: preal";
 by (rtac prealI2 1);
 by (rtac preal_sup_set_not_empty 1);
@@ -1209,27 +1209,27 @@
 by Auto_tac;
 qed "preal_sup1";
 
-Goalw [psup_def] "!!P. ? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
+Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
 by Auto_tac;
 qed "preal_psup_leI";
 
-Goalw [psup_def] "!!P. ? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
+Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 qed "preal_psup_leI2";
 
-Goal "!!P. [| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
+Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
 by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
 qed "preal_psup_leI2b";
 
-Goal "!!P. [| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
+Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
 by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
 qed "preal_psup_leI2a";
 
-Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
+Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
 by (rotate_tac 1 2);
@@ -1237,7 +1237,7 @@
 by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
 qed "psup_le_ub";
 
-Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
+Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
 by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
 by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
 by (rotate_tac 1 2);
@@ -1247,7 +1247,7 @@
 qed "psup_le_ub1";
 
 (** supremum property **)
-Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
+Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
 \         ==> (!Y. (? X: P. Y < X) = (Y < psup P))";              
 by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
 by (Fast_tac 1);
@@ -1267,12 +1267,12 @@
     (****** Embedding ******)
 (*** mapping from prat into preal ***)
 
-Goal "!!z1. x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
+Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
 by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
 qed "lemma_preal_rat_less";
 
-Goal "!!z1. x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
+Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
 by (stac prat_add_commute 1);
 by (dtac (prat_add_commute RS subst) 1);
 by (etac lemma_preal_rat_less 1);
@@ -1291,13 +1291,13 @@
      prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
 qed "preal_prat_add";
 
-Goal "!!xa. x < xa ==> x*z1*qinv(xa) < z1";
+Goal "x < xa ==> x*z1*qinv(xa) < z1";
 by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
 by (dtac (prat_mult_left_commute RS subst) 1);
 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
 qed "lemma_preal_rat_less3";
 
-Goal "!!xa. xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
+Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
 by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
 by (dtac (prat_mult_left_commute RS subst) 1);
 by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/RComplete.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -24,7 +24,7 @@
            Completeness theorem for the positive reals(again)
  ----------------------------------------------------------------*)
 
-Goal "!!S. [| ALL x: S. 0r < x; \
+Goal "[| ALL x: S. 0r < x; \
 \                 EX x. x: S; \
 \                 EX u. isUb (UNIV::real set) S u \
 \              |] ==> EX t. isLub (UNIV::real set) S t";
@@ -85,7 +85,7 @@
 by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
 qed "lemma_le_swap2";
 
-Goal "!!x. [| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
+Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
 by (dtac real_add_less_mono 1);
 by (assume_tac 1);
 by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1);
@@ -104,13 +104,13 @@
         real_add_minus_left,real_add_zero_left]) 1);
 qed "lemma_real_complete2";
 
-Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
+Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
 by (rtac (lemma_le_swap2 RS iffD2) 1);
 by (etac lemma_real_complete2 1);
 by (assume_tac 1);
 qed "lemma_real_complete2a";
 
-Goal "!!x. [| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
+Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
 by (rotate_tac 1 1);
 by (etac (real_le_imp_less_or_eq RS disjE) 1);
 by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
@@ -173,7 +173,7 @@
       real_add_minus,real_add_minus_left,real_add_zero_right]));
 qed "lemma_arch";
 
-Goal "!!x. 0r < x ==> EX n. rinv(%%#n) < x";
+Goal "0r < x ==> EX n. rinv(%%#n) < x";
 by (stac real_nat_rinv_Ex_iff 1);
 by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
 by (fold_tac [real_le_def]);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/Real.ML
--- a/src/HOL/Real/Real.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/Real.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -239,7 +239,7 @@
     real_add_zero_right,real_add_zero_left]) 1);
 qed "real_minus_left_ex1";
 
-Goal "!!y. x + y = 0r ==> x = %~y";
+Goal "x + y = 0r ==> x = %~y";
 by (cut_inst_tac [("z","y")] real_add_minus_left 1);
 by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
 by (Blast_tac 1);
@@ -451,19 +451,19 @@
               simpset() addsimps [real_mult_inv_left]));
 qed "real_mult_inv_right";
 
-Goal "!!a. (c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
+Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
 by Auto_tac;
 by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
 qed "real_mult_left_cancel";
     
-Goal "!!a. (c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
+Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
 by (Step_tac 1);
 by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
 qed "real_mult_right_cancel";
 
-Goalw [rinv_def] "!!x. x ~= 0r ==> rinv(x) ~= 0r";
+Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
 by (forward_tac [real_mult_inv_left_ex] 1);
 by (etac exE 1);
 by (rtac selectI2 1);
@@ -473,7 +473,7 @@
 
 Addsimps [real_mult_inv_left,real_mult_inv_right];
 
-Goal "!!x. x ~= 0r ==> rinv(rinv x) = x";
+Goal "x ~= 0r ==> rinv(rinv x) = x";
 by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
 by (etac rinv_not_zero 1);
 by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
@@ -488,7 +488,7 @@
     [real_zero_not_eq_one RS not_sym]));
 qed "real_rinv_1";
 
-Goal "!!x. x ~= 0r ==> rinv(%~x) = %~rinv(x)";
+Goal "x ~= 0r ==> rinv(%~x) = %~rinv(x)";
 by (res_inst_tac [("c1","%~x")] (real_mult_right_cancel RS iffD1) 1);
 by Auto_tac;
 qed "real_minus_rinv";
@@ -637,19 +637,19 @@
 qed "real_preal_trichotomy";
 
 Goal "!!x. [| !!m. x = %#m ==> P; \
-\            x = 0r ==> P; \
-\            !!m. x = %~(%#m) ==> P |] ==> P";
+\             x = 0r ==> P; \
+\             !!m. x = %~(%#m) ==> P |] ==> P";
 by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
 by Auto_tac;
 qed "real_preal_trichotomyE";
 
-Goalw [real_preal_def] "!!m1 m2. %#m1 < %#m2 ==> m1 < m2";
+Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
 by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
 by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
 qed "real_preal_lessD";
 
-Goal "!!m1 m2. m1 < m2 ==> %#m1 < %#m2";
+Goal "m1 < m2 ==> %#m1 < %#m2";
 by (dtac preal_less_add_left_Ex 1);
 by (auto_tac (claset(),simpset() addsimps [real_preal_add,
     real_preal_def,real_less_def]));
@@ -743,7 +743,7 @@
                addEs [real_less_irrefl]) 1);
 qed "real_preal_not_minus_gt_all";
 
-Goal "!!m1 m2. %~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
+Goal "%~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
 by (auto_tac (claset(),simpset() addsimps 
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
@@ -754,7 +754,7 @@
 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
 qed "real_preal_minus_less_rev1";
 
-Goal "!!m1 m2. %#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
+Goal "%#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
 by (auto_tac (claset(),simpset() addsimps 
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
@@ -790,25 +790,25 @@
 
 (*** Properties of <= ***)
 
-Goalw [real_le_def] "!!w. ~(w < z) ==> z <= (w::real)";
+Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
 by (assume_tac 1);
 qed "real_leI";
 
-Goalw [real_le_def] "!!w. z<=w ==> ~(w<(z::real))";
+Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
 by (assume_tac 1);
 qed "real_leD";
 
 val real_leE = make_elim real_leD;
 
-Goal "!!w. (~(w < z)) = (z <= (w::real))";
+Goal "(~(w < z)) = (z <= (w::real))";
 by (fast_tac (claset() addSIs [real_leI,real_leD]) 1);
 qed "real_less_le_iff";
 
-Goalw [real_le_def] "!!z. ~ z <= w ==> w<(z::real)";
+Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
 by (Fast_tac 1);
 qed "not_real_leE";
 
-Goalw [real_le_def] "!!z. z < w ==> z <= (w::real)";
+Goalw [real_le_def] "z < w ==> z <= (w::real)";
 by (fast_tac (claset() addEs [real_less_asym]) 1);
 qed "real_less_imp_le";
 
@@ -817,7 +817,7 @@
 by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
 qed "real_le_imp_less_or_eq";
 
-Goalw [real_le_def] "!!z. z<w | z=w ==> z <=(w::real)";
+Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
 by (cut_facts_tac [real_linear] 1);
 by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
 qed "real_less_or_eq_imp_le";
@@ -840,17 +840,17 @@
 by (fast_tac (claset() addIs [real_less_trans]) 1);
 qed "real_less_le_trans";
 
-Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::real)";
+Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
             rtac real_less_or_eq_imp_le, fast_tac (claset() addIs [real_less_trans])]);
 qed "real_le_trans";
 
-Goal "!!z. [| z <= w; w <= z |] ==> z = (w::real)";
+Goal "[| z <= w; w <= z |] ==> z = (w::real)";
 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
             fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
 qed "real_le_anti_sym";
 
-Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::real)";
+Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
 by (rtac not_real_leE 1);
 by (fast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
 qed "not_less_not_eq_real_less";
@@ -879,23 +879,23 @@
      real_preal_not_minus_gt_zero RS notE]) 1);
 qed "real_gt_zero_preal_Ex";
 
-Goal "!!x. %#z < x ==> ? y. x = %#y";
+Goal "%#z < x ==> ? y. x = %#y";
 by (blast_tac (claset() addSDs [real_preal_zero_less RS real_less_trans]
                addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
 qed "real_gt_preal_preal_Ex";
 
-Goal "!!x. %#z <= x ==> ? y. x = %#y";
+Goal "%#z <= x ==> ? y. x = %#y";
 by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
               real_gt_preal_preal_Ex]) 1);
 qed "real_ge_preal_preal_Ex";
 
-Goal "!!y. y <= 0r ==> !x. y < %#x";
+Goal "y <= 0r ==> !x. y < %#x";
 by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
               addIs [real_preal_zero_less RSN(2,real_less_trans)],
               simpset() addsimps [real_preal_zero_less]));
 qed "real_less_all_preal";
 
-Goal "!!y. ~ 0r < y ==> !x. y < %#x";
+Goal "~ 0r < y ==> !x. y < %#x";
 by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
 qed "real_less_all_real2";
 
@@ -937,19 +937,19 @@
 
 (* lemmas *)
 (** change naff name(s)! **)
-Goal "!!S. (W < S) ==> (0r < S + %~W)";
+Goal "(W < S) ==> (0r < S + %~W)";
 by (dtac real_less_add_positive_left_Ex 1);
 by (auto_tac (claset(),simpset() addsimps [real_add_minus,
     real_add_zero_right] @ real_add_ac));
 qed "real_less_sum_gt_zero";
 
 Goal "!!S. T = S + W ==> S = T + %~W";
-by (asm_simp_tac (simpset() addsimps [real_add_minus,
-    real_add_zero_right] @ real_add_ac) 1);
+by (asm_simp_tac (simpset() addsimps [real_add_minus, real_add_zero_right] 
+		                     @ real_add_ac) 1);
 qed "real_lemma_change_eq_subj";
 
 (* FIXME: long! *)
-Goal "!!W. (0r < S + %~W) ==> (W < S)";
+Goal "(0r < S + %~W) ==> (W < S)";
 by (rtac ccontr 1);
 by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
 by (auto_tac (claset(),
@@ -976,7 +976,7 @@
 by (simp_tac (simpset() addsimps [real_add_commute]) 1);
 qed "real_less_swap_iff";
 
-Goal "!!T. [| R + L = S; 0r < L |] ==> R < S";
+Goal "[| R + L = S; 0r < L |] ==> R < S";
 by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
 by (auto_tac (claset(),simpset() addsimps [
     real_add_minus,real_add_zero_right] @ real_add_ac));
@@ -1075,11 +1075,11 @@
 (*** Completeness of reals ***)
 (** use supremum property of preal and theorems about real_preal **)
               (*** a few lemmas ***)
-Goal "!!P y. ! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
+Goal "! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
 by (blast_tac (claset() addSDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
 qed "real_sup_lemma1";
 
-Goal "!!P. [| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
 \         ==> (? X. X: {w. %#w : P}) & (? Y. !X: {w. %#w : P}. X < Y)";
 by (rtac conjI 1);
 by (blast_tac (claset() addDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
@@ -1101,7 +1101,7 @@
 (* Supremum property for the set of positive reals *)
 (* FIXME: long proof - can be improved - need only have one case split *)
 (* will do for now *)
-Goal "!!P. [| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
+Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
 \         ==> (? S. !y. (? x: P. y < x) = (y < S))";
 by (res_inst_tac [("x","%#psup({w. %#w : P})")] exI 1);
 by Auto_tac;
@@ -1156,7 +1156,7 @@
     real_add_minus_left,real_add_zero_left]) 1);
 qed "real_less_add_left_cancel";
 
-Goal "!!x. [| 0r < x; 0r < y |] ==> 0r < x + y";
+Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
 by (REPEAT(dtac (real_gt_zero_preal_Ex RS iffD1) 1));
 by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
 by (Step_tac 1);
@@ -1267,7 +1267,7 @@
 by (Blast_tac 1);
 qed "real_nat_less_zero";
 
-Goal "!!n. 1r <= %%#n";
+Goal "1r <= %%#n";
 by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
 by (nat_ind_tac "n" 1);
 by (auto_tac (claset(),simpset () 
@@ -1284,7 +1284,7 @@
     real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
 qed "real_nat_rinv_not_zero";
 
-Goal "!!x. rinv(%%#x) = rinv(%%#y) ==> x = y";
+Goal "rinv(%%#x) = rinv(%%#y) ==> x = y";
 by (rtac (inj_real_nat RS injD) 1);
 by (res_inst_tac [("n2","x")] 
     (real_nat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
@@ -1294,7 +1294,7 @@
     real_not_refl2 RS not_sym)]) 1);
 qed "real_nat_rinv_inj";
 
-Goal "!!x. 0r < x ==> 0r < rinv x";
+Goal "0r < x ==> 0r < rinv x";
 by (EVERY1[rtac ccontr, dtac real_leI]);
 by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
 by (forward_tac [real_not_refl2 RS not_sym] 1);
@@ -1305,7 +1305,7 @@
     simpset() addsimps [real_minus_mult_eq1 RS sym]));
 qed "real_rinv_gt_zero";
 
-Goal "!!x. x < 0r ==> rinv x < 0r";
+Goal "x < 0r ==> rinv x < 0r";
 by (forward_tac [real_not_refl2] 1);
 by (dtac (real_minus_zero_less_iff RS iffD2) 1);
 by (rtac (real_minus_zero_less_iff RS iffD1) 1);
@@ -1370,12 +1370,12 @@
 by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
 qed "real_mult_less_cancel2";
 
-Goal "!!z. 0r < z ==> (x*z < y*z) = (x < y)";
+Goal "0r < z ==> (x*z < y*z) = (x < y)";
 by (blast_tac (claset() addIs [real_mult_less_mono1,
     real_mult_less_cancel1]) 1);
 qed "real_mult_less_iff1";
 
-Goal "!!z. 0r < z ==> (z*x < z*y) = (x < y)";
+Goal "0r < z ==> (z*x < z*y) = (x < y)";
 by (blast_tac (claset() addIs [real_mult_less_mono2,
     real_mult_less_cancel2]) 1);
 qed "real_mult_less_iff2";
@@ -1432,7 +1432,7 @@
 
 Addsimps [real_nat_less_iff];
 
-Goal "!!u. 0r < u  ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
+Goal "0r < u  ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
 by (Step_tac 1);
 by (res_inst_tac [("n2","n")] (real_nat_less_zero RS 
     real_rinv_gt_zero RS real_mult_less_cancel1) 1);
@@ -1447,7 +1447,7 @@
     real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
 qed "real_nat_less_rinv_iff";
 
-Goal "!!x. 0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
+Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
 by (auto_tac (claset(),simpset() addsimps [real_rinv_rinv,
     real_nat_less_zero,real_not_refl2 RS not_sym]));
 qed "real_nat_rinv_eq_iff";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Real/RealAbs.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -37,7 +37,7 @@
 by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
 qed "rabs_minus_eqI2";
 
-Goal "!!x. x<=0r ==> rabs x = %~x";
+Goal "x<=0r ==> rabs x = %~x";
 by (dtac real_le_imp_less_or_eq 1);
 by (fast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
 qed "rabs_minus_eqI1";
@@ -86,7 +86,7 @@
     simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
 qed "rabs_mult";
 
-Goalw [rabs_def] "!!x. x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
+Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
 by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] 
     setloop (split_tac [expand_if])));
 by (ALLGOALS(dtac not_real_leE));
@@ -142,7 +142,7 @@
 by (REPEAT (ares_tac [real_add_less_mono] 1));
 qed "rabs_add_less";
 
-Goal "!!x y. [| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
+Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
 by (rotate_tac 1 1);
 by (dtac (rabs_minus_cancel RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
@@ -175,13 +175,13 @@
 			     real_le_less_trans]) 1);
 qed "rabs_mult_less";
 
-Goal "!!x. [| rabs x < r; rabs y < s |] \
+Goal "[| rabs x < r; rabs y < s |] \
 \          ==> rabs(x)*rabs(y)<r*s";
 by (auto_tac (claset() addIs [rabs_mult_less],
               simpset() addsimps [rabs_mult RS sym]));
 qed "rabs_mult_less2";
 
-Goal "!! x y r. 1r < rabs x ==> rabs y <= rabs(x*y)";
+Goal "1r < rabs x ==> rabs y <= rabs(x*y)";
 by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1);
 by (EVERY1[etac disjE,rtac real_less_imp_le]);
 by (dres_inst_tac [("W","1r")]  real_less_sum_gt_zero 1);
@@ -194,11 +194,11 @@
 by (asm_full_simp_tac (simpset() addsimps [real_le_refl,rabs_mult]) 1);
 qed "rabs_mult_le";
 
-Goal "!!x. [| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
+Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
 by (fast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1);
 qed "rabs_mult_gt";
 
-Goal "!!r. rabs(x)<r ==> 0r<r";
+Goal "rabs(x)<r ==> 0r<r";
 by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1);
 qed "rabs_less_gt_zero";
 
@@ -217,7 +217,7 @@
                             rabs_zero,rabs_minus_zero]) 1);
 qed "rabs_disj";
 
-Goal "!!x. rabs x = y ==> x = y | %~x = y";
+Goal "rabs x = y ==> x = y | %~x = y";
 by (dtac sym 1);
 by (hyp_subst_tac 1);
 by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/RelPow.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -15,7 +15,7 @@
 by (Simp_tac 1);
 qed "rel_pow_0_I";
 
-Goal "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
+Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
 by (Simp_tac  1);
 by (Blast_tac 1);
 qed "rel_pow_Suc_I";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Relation.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -68,7 +68,7 @@
 by (Blast_tac 1);
 qed "O_assoc";
 
-Goal "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
+Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (Blast_tac 1);
 qed "comp_mono";
 
@@ -91,17 +91,17 @@
 
 (** Natural deduction for r^-1 **)
 
-Goalw [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
+Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
 by (Simp_tac 1);
 qed "converse_iff";
 
 AddIffs [converse_iff];
 
-Goalw [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
+Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
 by (Simp_tac 1);
 qed "converseI";
 
-Goalw [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
+Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
 by (Blast_tac 1);
 qed "converseD";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Set.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -13,7 +13,7 @@
 Addsimps [Collect_mem_eq];
 AddIffs  [mem_Collect_eq];
 
-Goal "!!a. P(a) ==> a : {x. P(x)}";
+Goal "P(a) ==> a : {x. P(x)}";
 by (Asm_simp_tac 1);
 qed "CollectI";
 
@@ -325,11 +325,11 @@
 
 Addsimps [Un_iff];
 
-Goal "!!c. c:A ==> c : A Un B";
+Goal "c:A ==> c : A Un B";
 by (Asm_simp_tac 1);
 qed "UnI1";
 
-Goal "!!c. c:B ==> c : A Un B";
+Goal "c:B ==> c : A Un B";
 by (Asm_simp_tac 1);
 qed "UnI2";
 
@@ -356,15 +356,15 @@
 
 Addsimps [Int_iff];
 
-Goal "!!c. [| c:A;  c:B |] ==> c : A Int B";
+Goal "[| c:A;  c:B |] ==> c : A Int B";
 by (Asm_simp_tac 1);
 qed "IntI";
 
-Goal "!!c. c : A Int B ==> c:A";
+Goal "c : A Int B ==> c:A";
 by (Asm_full_simp_tac 1);
 qed "IntD1";
 
-Goal "!!c. c : A Int B ==> c:B";
+Goal "c : A Int B ==> c:B";
 by (Asm_full_simp_tac 1);
 qed "IntD2";
 
@@ -436,7 +436,7 @@
 qed_goal "singletonI" Set.thy "a : {a}"
  (fn _=> [ (rtac insertI1 1) ]);
 
-Goal "!!a. b : {a} ==> b=a";
+Goal "b : {a} ==> b=a";
 by (Blast_tac 1);
 qed "singletonD";
 
@@ -445,7 +445,7 @@
 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
 (fn _ => [Blast_tac 1]);
 
-Goal "!!a b. {a}={b} ==> a=b";
+Goal "{a}={b} ==> a=b";
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "singleton_inject";
 
@@ -469,7 +469,7 @@
 Addsimps [UN_iff];
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
-Goal "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
+Goal "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
 by Auto_tac;
 qed "UN_I";
 
@@ -504,7 +504,7 @@
 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
 qed "INT_I";
 
-Goal "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
+Goal "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
 by Auto_tac;
 qed "INT_D";
 
@@ -536,7 +536,7 @@
 Addsimps [Union_iff];
 
 (*The order of the premises presupposes that C is rigid; A may be flexible*)
-Goal "!!X. [| X:C;  A:X |] ==> A : Union(C)";
+Goal "[| X:C;  A:X |] ==> A : Union(C)";
 by Auto_tac;
 qed "UnionI";
 
@@ -565,7 +565,7 @@
 
 (*A "destruct" rule -- every X in C contains A as an element, but
   A:X can hold when X:C does not!  This rule is analogous to "spec". *)
-Goal "!!X. [| A : Inter(C);  X:C |] ==> A:X";
+Goal "[| A : Inter(C);  X:C |] ==> A:X";
 by Auto_tac;
 qed "InterD";
 
@@ -626,7 +626,7 @@
 
 (*** Range of a function -- just a translation for image! ***)
 
-Goal "!!b. b=f(x) ==> b : range(f)";
+Goal "b=f(x) ==> b : range(f)";
 by (EVERY1 [etac image_eqI, rtac UNIV_I]);
 bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Sexp.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -124,7 +124,7 @@
 by (rtac sexp_case_Numb 1);
 qed "sexp_rec_Numb";
 
-Goal "!!M. [| M: sexp;  N: sexp |] ==> \
+Goal "[| M: sexp;  N: sexp |] ==> \
 \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
 by (rtac (sexp_rec_unfold RS trans) 1);
 by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Sum.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -91,11 +91,11 @@
 
 (** Introduction rules for the injections **)
 
-Goalw [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
+Goalw [sum_def] "a : A ==> Inl(a) : A Plus B";
 by (Blast_tac 1);
 qed "InlI";
 
-Goalw [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
+Goalw [sum_def] "b : B ==> Inr(b) : A Plus B";
 by (Blast_tac 1);
 qed "InrI";
 
@@ -189,13 +189,13 @@
 by (rtac Int_lower1 1);
 qed "Part_subset";
 
-Goal "!!A B. A<=B ==> Part A h <= Part B h";
+Goal "A<=B ==> Part A h <= Part B h";
 by (Blast_tac 1);
 qed "Part_mono";
 
 val basic_monos = basic_monos @ [Part_mono];
 
-Goalw [Part_def] "!!a. a : Part A h ==> a : A";
+Goalw [Part_def] "a : Part A h ==> a : A";
 by (etac IntD1 1);
 qed "PartD1";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/TLA/hypsubst.ML
--- a/src/HOL/TLA/hypsubst.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/TLA/hypsubst.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -17,10 +17,10 @@
 
 Test data:
 
-Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
-Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
-Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
-Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
+Goal "[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
+Goal "[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
+Goal "[| ?x=y; P(?x) |] ==> y = a";
+Goal "[| ?x=y; P(?x) |] ==> y = a";
 
 by (hyp_subst_tac 1);
 by (bound_hyp_subst_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Trancl.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -28,7 +28,7 @@
 
 
 (*Closure under composition with r*)
-Goal "!!r. [| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
+Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
 by (stac rtrancl_unfold 1);
 by (Blast_tac 1);
 qed "rtrancl_into_rtrancl";
@@ -40,7 +40,7 @@
 qed "r_into_rtrancl";
 
 (*monotonicity of rtrancl*)
-Goalw [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*";
+Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
 by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
 qed "rtrancl_mono";
 
@@ -120,19 +120,19 @@
 qed "rtrancl_idemp_self_comp";
 Addsimps [rtrancl_idemp_self_comp];
 
-Goal "!!r s. r <= s^* ==> r^* <= s^*";
+Goal "r <= s^* ==> r^* <= s^*";
 by (dtac rtrancl_mono 1);
 by (Asm_full_simp_tac 1);
 qed "rtrancl_subset_rtrancl";
 
-Goal "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
+Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
 by (dtac rtrancl_mono 1);
 by (dtac rtrancl_mono 1);
 by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
 qed "rtrancl_subset";
 
-Goal "!!R. (R^* Un S^*)^* = (R Un S)^*";
+Goal "(R^* Un S^*)^* = (R Un S)^*";
 by (blast_tac (claset() addSIs [rtrancl_subset]
                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
 qed "rtrancl_Un_rtrancl";
@@ -143,14 +143,14 @@
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];
 
-Goal "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
+Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
 by (rtac converseI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseD";
 
-Goal "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
+Goal "(x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
 by (dtac converseD 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
@@ -204,7 +204,7 @@
 
 (**** The relation trancl ****)
 
-Goalw [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
+Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
 by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
 qed "trancl_mono";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Univ.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -142,11 +142,11 @@
 
 (** Injectiveness of Scons **)
 
-Goalw [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
+Goalw [Scons_def] "M$N <= M'$N' ==> M<=M'";
 by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma1";
 
-Goalw [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
+Goalw [Scons_def] "M$N <= M'$N' ==> N<=N'";
 by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
@@ -297,7 +297,7 @@
 
 (*** Cartesian Product ***)
 
-Goalw [uprod_def] "!!M N. [| M:A;  N:B |] ==> (M$N) : A<*>B";
+Goalw [uprod_def] "[| M:A;  N:B |] ==> (M$N) : A<*>B";
 by (REPEAT (ares_tac [singletonI,UN_I] 1));
 qed "uprodI";
 
@@ -322,11 +322,11 @@
 
 (*** Disjoint Sum ***)
 
-Goalw [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
+Goalw [usum_def] "M:A ==> In0(M) : A<+>B";
 by (Blast_tac 1);
 qed "usum_In0I";
 
-Goalw [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
+Goalw [usum_def] "N:B ==> In1(N) : A<+>B";
 by (Blast_tac 1);
 qed "usum_In1I";
 
@@ -408,23 +408,23 @@
 
 (*** Monotonicity ***)
 
-Goalw [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
+Goalw [uprod_def] "[| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
 by (Blast_tac 1);
 qed "uprod_mono";
 
-Goalw [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
+Goalw [usum_def] "[| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
 by (Blast_tac 1);
 qed "usum_mono";
 
-Goalw [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
+Goalw [Scons_def] "[| M<=M';  N<=N' |] ==> M$N <= M'$N'";
 by (Blast_tac 1);
 qed "Scons_mono";
 
-Goalw [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
+Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)";
 by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
 qed "In0_mono";
 
-Goalw [In1_def] "!!M N. M<=N ==> In1(M) <= In1(N)";
+Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)";
 by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
 qed "In1_mono";
 
@@ -471,7 +471,7 @@
 
 (*** Equality : the diagonal relation ***)
 
-Goalw [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
+Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
 by (Blast_tac 1);
 qed "diag_eqI";
 
@@ -506,11 +506,11 @@
 
 (*** Equality for Disjoint Sum ***)
 
-Goalw [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
+Goalw [dsum_def]  "(M,M'):r ==> (In0(M), In0(M')) : r<++>s";
 by (Blast_tac 1);
 qed "dsum_In0I";
 
-Goalw [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
+Goalw [dsum_def]  "(N,N'):s ==> (In1(N), In1(N')) : r<++>s";
 by (Blast_tac 1);
 qed "dsum_In1I";
 
@@ -531,11 +531,11 @@
 
 (*** Monotonicity ***)
 
-Goal "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
+Goal "[| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
 by (Blast_tac 1);
 qed "dprod_mono";
 
-Goal "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
+Goal "[| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
 by (Blast_tac 1);
 qed "dsum_mono";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/Vimage.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -102,6 +102,6 @@
 
 (** monotonicity **)
 
-Goal "!!f. A<=B ==> f-``A <= f-``B";
+Goal "A<=B ==> f-``A <= f-``B";
 by (Blast_tac 1);
 qed "vimage_mono";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/W0/MiniML.ML
--- a/src/HOL/W0/MiniML.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/W0/MiniML.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -11,7 +11,7 @@
 
 
 (* has_type is closed w.r.t. substitution *)
-Goal "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
+Goal "a |- e :: t ==> $s a |- e :: $s t";
 by (etac has_type.induct 1);
 (* case VarI *)
 by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/WF.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -93,7 +93,7 @@
  * Wellfoundedness of subsets
  *---------------------------------------------------------------------------*)
 
-Goal "!!r. [| wf(r);  p<=r |] ==> wf(p)";
+Goal "[| wf(r);  p<=r |] ==> wf(p)";
 by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
 by (Fast_tac 1);
 qed "wf_subset";
@@ -164,7 +164,7 @@
 by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
 qed "cuts_eq";
 
-Goalw [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
+Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)";
 by (asm_simp_tac HOL_ss 1);
 qed "cut_apply";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/WF_Rel.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -32,7 +32,7 @@
  * The inverse image into a wellfounded relation is wellfounded.
  *---------------------------------------------------------------------------*)
 
-Goal "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
+Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
 by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
 by (Clarify_tac 1);
 by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
@@ -110,7 +110,7 @@
  * Cannot go into WF because it needs Finite
  *---------------------------------------------------------------------------*)
 
-Goal "!!r. finite r ==> acyclic r --> wf r";
+Goal "finite r ==> acyclic r --> wf r";
 by (etac finite_induct 1);
  by (Blast_tac 1);
 by (split_all_tac 1);
@@ -122,7 +122,7 @@
 	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
 	etac (acyclic_converse RS iffD2) 1]);
 
-Goal "!!r. finite r ==> wf r = acyclic r";
+Goal "finite r ==> wf r = acyclic r";
 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
 qed "wf_iff_acyclic_if_finite";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/equalities.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -51,7 +51,7 @@
 bind_thm("empty_not_insert",insert_not_empty RS not_sym);
 Addsimps[empty_not_insert];
 
-Goal "!!a. a:A ==> insert a A = A";
+Goal "a:A ==> insert a A = A";
 by (Blast_tac 1);
 qed "insert_absorb";
 (* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
@@ -72,12 +72,12 @@
 qed "insert_subset";
 Addsimps[insert_subset];
 
-Goal "!!a. insert a A ~= insert a B ==> A ~= B";
+Goal "insert a A ~= insert a B ==> A ~= B";
 by (Blast_tac 1);
 qed "insert_lim";
 
 (* use new B rather than (A-{a}) to avoid infinite unfolding *)
-Goal "!!a. a:A ==> ? B. A = insert a B & a ~: B";
+Goal "a:A ==> ? B. A = insert a B & a ~: B";
 by (res_inst_tac [("x","A-{a}")] exI 1);
 by (Blast_tac 1);
 qed "mk_disjoint_insert";
@@ -114,7 +114,7 @@
 by (Blast_tac 1);
 qed "image_image";
 
-Goal "!!x. x:A ==> insert (f x) (f``A) = f``A";
+Goal "x:A ==> insert (f x) (f``A) = f``A";
 by (Blast_tac 1);
 qed "insert_image";
 Addsimps [insert_image];
@@ -164,11 +164,11 @@
 (*Intersection is an AC-operator*)
 val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
 
-Goal "!!A B. B<=A ==> A Int B = B";
+Goal "B<=A ==> A Int B = B";
 by (Blast_tac 1);
 qed "Int_absorb1";
 
-Goal "!!A B. A<=B ==> A Int B = A";
+Goal "A<=B ==> A Int B = A";
 by (Blast_tac 1);
 qed "Int_absorb2";
 
@@ -243,11 +243,11 @@
 (*Union is an AC-operator*)
 val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
 
-Goal "!!A B. A<=B ==> A Un B = B";
+Goal "A<=B ==> A Un B = B";
 by (Blast_tac 1);
 qed "Un_absorb1";
 
-Goal "!!A B. B<=A ==> A Un B = A";
+Goal "B<=A ==> A Un B = A";
 by (Blast_tac 1);
 qed "Un_absorb2";
 
@@ -446,7 +446,7 @@
 qed "UN_singleton";
 Addsimps [UN_singleton];
 
-Goal "!!k. k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
+Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
 by (Blast_tac 1);
 qed "UN_absorb";
 
@@ -455,7 +455,7 @@
 qed "INT_empty";
 Addsimps[INT_empty];
 
-Goal "!!k. k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
+Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
 by (Blast_tac 1);
 qed "INT_absorb";
 
@@ -490,12 +490,12 @@
 by (Blast_tac 1);
 qed "Inter_image_eq";
 
-Goal "!!A. A~={} ==> (UN y:A. c) = c";
+Goal "A~={} ==> (UN y:A. c) = c";
 by (Blast_tac 1);
 qed "UN_constant";
 Addsimps[UN_constant];
 
-Goal "!!A. A~={} ==> (INT y:A. c) = c";
+Goal "A~={} ==> (INT y:A. c) = c";
 by (Blast_tac 1);
 qed "INT_constant";
 Addsimps[INT_constant];
@@ -601,7 +601,7 @@
 qed "Diff_cancel";
 Addsimps[Diff_cancel];
 
-Goal "!!A B. A Int B = {} ==> A-B = A";
+Goal "A Int B = {} ==> A-B = A";
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "Diff_triv";
 
@@ -620,7 +620,7 @@
 qed "Diff_UNIV";
 Addsimps[Diff_UNIV];
 
-Goal "!!x. x~:A ==> A - insert x B = A-B";
+Goal "x~:A ==> A - insert x B = A-B";
 by (Blast_tac 1);
 qed "Diff_insert0";
 Addsimps [Diff_insert0];
@@ -640,12 +640,12 @@
 by (Blast_tac 1);
 qed "insert_Diff_if";
 
-Goal "!!x. x:B ==> insert x A - B = A-B";
+Goal "x:B ==> insert x A - B = A-B";
 by (Blast_tac 1);
 qed "insert_Diff1";
 Addsimps [insert_Diff1];
 
-Goal "!!a. a:A ==> insert a (A-{a}) = A";
+Goal "a:A ==> insert a (A-{a}) = A";
 by (Blast_tac 1);
 qed "insert_Diff";
 
@@ -654,11 +654,11 @@
 qed "Diff_disjoint";
 Addsimps[Diff_disjoint];
 
-Goal "!!A. A<=B ==> A Un (B-A) = B";
+Goal "A<=B ==> A Un (B-A) = B";
 by (Blast_tac 1);
 qed "Diff_partition";
 
-Goal "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
+Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
 by (Blast_tac 1);
 qed "double_diff";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/Fib.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -45,7 +45,7 @@
 (* Also add  0 < fib (Suc n) *)
 Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
 
-Goal "!!n. 0<n ==> 0 < fib n";
+Goal "0<n ==> 0 < fib n";
 by (rtac (not0_implies_Suc RS exE) 1);
 by Auto_tac;
 qed "fib_gr_0";
@@ -93,12 +93,12 @@
 by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
 qed "gcd_fib_add";
 
-Goal "!!m. m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
+Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
 by (rtac (gcd_fib_add RS sym RS trans) 1);
 by (Asm_simp_tac 1);
 qed "gcd_fib_diff";
 
-Goal "!!m. 0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
+Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
 by (res_inst_tac [("n","n")] less_induct 1);
 by (stac mod_if 1);
 by (Asm_simp_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/InSort.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -32,7 +32,7 @@
 qed "sorted_ins";
 Addsimps [sorted_ins];
 
-Goal "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
+Goal "[| total(f); transf(f) |] ==>  sorted f (insort f xs)";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "sorted_insort";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/MT.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -574,7 +574,7 @@
 
 (* Introduction rules for hasty *)
 
-Goalw [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
+Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
 by (etac hasty_rel_const_coind 1);
 qed "hasty_const";
 
@@ -592,7 +592,7 @@
 by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
 qed "hasty_elim_const_lem";
 
-Goal "!!c. v_const(c) hasty t ==> c isof t";
+Goal "v_const(c) hasty t ==> c isof t";
 by (dtac hasty_elim_const_lem 1);
 by (Blast_tac 1);
 qed "hasty_elim_const";
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/Primes.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -46,7 +46,7 @@
 qed "gcd_0";
 Addsimps [gcd_0];
 
-Goal "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
+Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
 by (rtac (gcd_eq RS trans) 1);
 by (Asm_simp_tac 1);
 by (Blast_tac 1);
@@ -71,7 +71,7 @@
 
 (*Maximality: for all m,n,f naturals, 
                 if f divides m and f divides n then f divides gcd(m,n)*)
-Goal "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
+Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
 by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
 by (ALLGOALS
     (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod,
@@ -84,7 +84,7 @@
 qed "is_gcd";
 
 (*uniqueness of GCDs*)
-Goalw [is_gcd_def] "!!m n. [| is_gcd m a b; is_gcd n a b |] ==> m=n";
+Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n";
 by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
 qed "is_gcd_unique";
 
@@ -150,20 +150,20 @@
 qed "gcd_mult";
 Addsimps [gcd_mult];
 
-Goal "!!k. [| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
+Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
 by (subgoal_tac "m = gcd(m*k, m*n)" 1);
 by (etac ssubst 1 THEN rtac gcd_greatest 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
 qed "relprime_dvd_mult";
 
-Goalw [prime_def] "!!p. [| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
+Goalw [prime_def] "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
 by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
-by (fast_tac (claset() addss (simpset())) 1);
+by Auto_tac;
 qed "prime_imp_relprime";
 
 (*This theorem leads immediately to a proof of the uniqueness of factorization.
   If p divides a product of primes then it is one of those primes.*)
-Goal "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
+Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
 by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1);
 qed "prime_dvd_mult";
 
@@ -192,7 +192,7 @@
                                gcd_dvd1, gcd_dvd2]) 1);
 qed "gcd_dvd_gcd_mult";
 
-Goal "!!n. gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
+Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
 by (rtac dvd_anti_sym 1);
 by (rtac gcd_dvd_gcd_mult 2);
 by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOL/ex/Primrec.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -71,7 +71,7 @@
 qed_spec_mp "ack_less_mono2";
 
 (*PROPERTY A 5', monotonicity for<=*)
-Goal "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)";
+Goal "j<=k ==> ack(i,j)<=ack(i,k)";
 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 by (blast_tac (claset() addIs [ack_less_mono2]) 1);
 qed "ack_le_mono2";
@@ -127,13 +127,13 @@
 by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
 val lemma = result();
 
-Goal "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
+Goal "i<j ==> ack(i,k) < ack(j,k)";
 by (dtac less_eq_Suc_add 1);
 by (blast_tac (claset() addSIs [lemma]) 1);
 qed "ack_less_mono1";
 
 (*PROPERTY A 7', monotonicity for<=*)
-Goal "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)";
+Goal "i<=j ==> ack(i,k)<=ack(j,k)";
 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 by (blast_tac (claset() addIs [ack_less_mono1]) 1);
 qed "ack_le_mono1";
@@ -160,7 +160,7 @@
 
 (*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   used k+4.  Quantified version must be nested EX k'. ALL i,j... *)
-Goal "!!i j k. i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
+Goal "i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
 by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1);
 by (rtac (ack_add_bound RS less_le_trans) 2);
 by (Asm_simp_tac 2);
@@ -254,7 +254,7 @@
 by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1));
 qed "PREC_case";
 
-Goal "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
+Goal "f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
 by (etac PRIMREC.induct 1);
 by (ALLGOALS 
     (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Fix.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -884,7 +884,7 @@
         (Simp_tac 1)
         ]);
 
-Goal "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
+Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
 \           ==> adm (%x. P x = Q x)";
 by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
 by (Asm_simp_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -22,7 +22,7 @@
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
-Goal "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
+Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
 by (etac evalc.induct 1);
       by (ALLGOALS Asm_simp_tac);
  by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -36,9 +36,7 @@
 
 Goal "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
 \   cont (%y. lift_case UU (f y) (g y))";
-by (rtac cont2cont_app 1);
-back();
-by (safe_tac set_cs);
+by (res_inst_tac [("tt","g")] cont2cont_app 1);
 by (rtac cont_flift1_not_arg 1);
 by Auto_tac;
 by (rtac cont_flift1_arg 1);
@@ -100,7 +98,7 @@
 
 Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
 
-Goal "!!x. x~=UU ==> (flift2 f)`x~=UU";
+Goal "x~=UU ==> (flift2 f)`x~=UU";
 by (def_tac 1);
 qed"flift2_nUU";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift2.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -44,7 +44,7 @@
 
 (* Tailoring notUU_I of Pcpo.ML to Undef *)
 
-Goal "!!x. [| x<<y; ~x=Undef |] ==> ~y=Undef";
+Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
 by (etac contrapos 1);
 by (hyp_subst_tac 1);
 by (rtac antisym_less 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -139,13 +139,13 @@
 
 (* Two specific lemmas for the combination of LCF and HOL terms *)
 
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
 by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
 by Auto_tac;
 qed"cont_fapp_app";
 
-Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
+Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
 by (rtac cont2cont_CF1L 1);
 by (etac cont_fapp_app 1);
 by (assume_tac 1);
diff -r c56aa8b59dc0 -r b94cd208f073 src/HOLCF/Tr.ML
--- a/src/HOLCF/Tr.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/HOLCF/Tr.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -120,7 +120,7 @@
 by Auto_tac;
 qed"andalso_or";
 
-Goal "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
+Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
 by (rtac iffI 1);
 by (res_inst_tac [("p","t")] trE 1);
 by Auto_tac;
@@ -176,12 +176,12 @@
 val adm_tricks = [adm_trick_1,adm_trick_2];
 
 
-Goal "!!f. cont(f) ==> adm (%x. (f x)~=TT)";
+Goal "cont(f) ==> adm (%x. (f x)~=TT)";
 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
 qed"adm_nTT";
 
-Goal "!!f. cont(f) ==> adm (%x. (f x)~=FF)";
+Goal "cont(f) ==> adm (%x. (f x)~=FF)";
 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
 qed"adm_nFF";
diff -r c56aa8b59dc0 -r b94cd208f073 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Cardinal.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -257,7 +257,7 @@
 
 (*Need AC to get X lepoll Y ==> |X| le |Y|;  see well_ord_lepoll_imp_Card_le
   Converse also requires AC, but see well_ord_cardinal_eqE*)
-Goalw [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
+Goalw [eqpoll_def,cardinal_def] "X eqpoll Y ==> |X| = |Y|";
 by (rtac Least_cong 1);
 by (blast_tac (claset() addIs [comp_bij, bij_converse_bij]) 1);
 qed "cardinal_cong";
diff -r c56aa8b59dc0 -r b94cd208f073 src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Coind/Map.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -82,7 +82,7 @@
 (* Monotonicity                                                 *)
 (* ############################################################ *)
 
-Goalw [PMap_def,TMap_def] "!!A. B<=C ==> PMap(A,B)<=PMap(A,C)";
+Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
 by (Fast_tac 1);
 qed "map_mono";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Ordinal.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -103,7 +103,7 @@
 
 (*** Lemmas for ordinals ***)
 
-Goalw [Ord_def,Transset_def] "!!i j.[| Ord(i);  j:i |] ==> Ord(j)";
+Goalw [Ord_def,Transset_def] "[| Ord(i);  j:i |] ==> Ord(j)";
 by (Blast_tac 1);
 qed "Ord_in_Ord";
 
@@ -117,7 +117,7 @@
      ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
 qed "Ord_subset_Ord";
 
-Goalw [Ord_def,Transset_def] "!!i j. [| j:i;  Ord(i) |] ==> j<=i";
+Goalw [Ord_def,Transset_def] "[| j:i;  Ord(i) |] ==> j<=i";
 by (Blast_tac 1);
 qed "OrdmemD";
 
diff -r c56aa8b59dc0 -r b94cd208f073 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/ZF/Perm.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -133,7 +133,7 @@
 by (rtac (prem RS lam_mono) 1);
 qed "id_mono";
 
-Goalw [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)";
+Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
 by (REPEAT (ares_tac [CollectI,lam_type] 1));
 by (etac subsetD 1 THEN assume_tac 1);
 by (Simp_tac 1);