Removal of leading "\!\!..." from most Goal commands
authorpaulson
Wed Jul 15 10:15:13 1998 +0200 (1998-07-15)
changeset 5143b94cd208f073
parent 5142 c56aa8b59dc0
child 5144 7ac22e5a05d7
Removal of leading "\!\!..." from most Goal commands
src/CCL/Set.ML
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/IOA/Asig.ML
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/Induct/Acc.ML
src/HOL/Induct/Com.ML
src/HOL/Induct/Comb.ML
src/HOL/Induct/Exp.ML
src/HOL/Induct/LFilter.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Mutil.ML
src/HOL/Induct/Perm.ML
src/HOL/Induct/PropLog.ML
src/HOL/Induct/SList.ML
src/HOL/Induct/Simult.ML
src/HOL/Induct/Term.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Integ.ML
src/HOL/Map.ML
src/HOL/NatDef.ML
src/HOL/Ord.ML
src/HOL/Power.ML
src/HOL/Prod.ML
src/HOL/Real/Lubs.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/Real.ML
src/HOL/Real/RealAbs.ML
src/HOL/RelPow.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sexp.ML
src/HOL/Sum.ML
src/HOL/TLA/hypsubst.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/Vimage.ML
src/HOL/W0/MiniML.ML
src/HOL/WF.ML
src/HOL/WF_Rel.ML
src/HOL/equalities.ML
src/HOL/ex/Fib.ML
src/HOL/ex/InSort.ML
src/HOL/ex/MT.ML
src/HOL/ex/Primes.ML
src/HOL/ex/Primrec.ML
src/HOLCF/Fix.ML
src/HOLCF/IMP/Denotational.ML
src/HOLCF/Lift.ML
src/HOLCF/Lift2.ML
src/HOLCF/Lift3.ML
src/HOLCF/Tr.ML
src/ZF/Cardinal.ML
src/ZF/Coind/Map.ML
src/ZF/Ordinal.ML
src/ZF/Perm.ML
     1.1 --- a/src/CCL/Set.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/CCL/Set.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  qed_goal "subset_refl" Set.thy "A <= A"
     1.5   (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
     1.6  
     1.7 -Goal "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
     1.8 +Goal "[| A<=B;  B<=C |] ==> A<=C";
     1.9  by (rtac subsetI 1);
    1.10  by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
    1.11  qed "subset_trans";
     2.1 --- a/src/HOL/Arith.ML	Tue Jul 14 13:33:12 1998 +0200
     2.2 +++ b/src/HOL/Arith.ML	Wed Jul 15 10:15:13 1998 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  (* Could be (and is, below) generalized in various ways;
     2.5     However, none of the generalizations are currently in the simpset,
     2.6     and I dread to think what happens if I put them in *)
     2.7 -Goal "!!n. 0 < n ==> Suc(n-1) = n";
     2.8 +Goal "0 < n ==> Suc(n-1) = n";
     2.9  by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
    2.10  qed "Suc_pred";
    2.11  Addsimps [Suc_pred];
    2.12 @@ -111,7 +111,7 @@
    2.13  Addsimps [pred_add_is_0];
    2.14  
    2.15  (* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    2.16 -Goal "!!n. 0<n ==> m + (n-1) = (m+n)-1";
    2.17 +Goal "0<n ==> m + (n-1) = (m+n)-1";
    2.18  by (exhaust_tac "m" 1);
    2.19  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    2.20                                        addsplits [split_nat_case])));
    2.21 @@ -128,7 +128,7 @@
    2.22  (**** Additional theorems about "less than" ****)
    2.23  
    2.24  (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
    2.25 -Goal "!!m. m<n --> (? k. n=Suc(m+k))";
    2.26 +Goal "m<n --> (? k. n=Suc(m+k))";
    2.27  by (induct_tac "n" 1);
    2.28  by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    2.29  by (blast_tac (claset() addSEs [less_SucE] 
    2.30 @@ -162,7 +162,7 @@
    2.31  (*"i < j ==> i < m+j"*)
    2.32  bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
    2.33  
    2.34 -Goal "!!i. i+j < (k::nat) ==> i<k";
    2.35 +Goal "i+j < (k::nat) ==> i<k";
    2.36  by (etac rev_mp 1);
    2.37  by (induct_tac "j" 1);
    2.38  by (ALLGOALS Asm_simp_tac);
    2.39 @@ -328,11 +328,11 @@
    2.40  by (ALLGOALS Asm_simp_tac);
    2.41  qed_spec_mp "add_diff_inverse";
    2.42  
    2.43 -Goal "!!m. n<=m ==> n+(m-n) = (m::nat)";
    2.44 +Goal "n<=m ==> n+(m-n) = (m::nat)";
    2.45  by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
    2.46  qed "le_add_diff_inverse";
    2.47  
    2.48 -Goal "!!m. n<=m ==> (m-n)+n = (m::nat)";
    2.49 +Goal "n<=m ==> (m-n)+n = (m::nat)";
    2.50  by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
    2.51  qed "le_add_diff_inverse2";
    2.52  
    2.53 @@ -372,7 +372,7 @@
    2.54  qed "Suc_diff_diff";
    2.55  Addsimps [Suc_diff_diff];
    2.56  
    2.57 -Goal "!!n. 0<n ==> n - Suc i < n";
    2.58 +Goal "0<n ==> n - Suc i < n";
    2.59  by (res_inst_tac [("n","n")] natE 1);
    2.60  by Safe_tac;
    2.61  by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
    2.62 @@ -557,13 +557,13 @@
    2.63  qed "mult_eq_1_iff";
    2.64  Addsimps [mult_eq_1_iff];
    2.65  
    2.66 -Goal "!!k. 0<k ==> (m*k < n*k) = (m<n)";
    2.67 +Goal "0<k ==> (m*k < n*k) = (m<n)";
    2.68  by (safe_tac (claset() addSIs [mult_less_mono1]));
    2.69  by (cut_facts_tac [less_linear] 1);
    2.70  by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
    2.71  qed "mult_less_cancel2";
    2.72  
    2.73 -Goal "!!k. 0<k ==> (k*m < k*n) = (m<n)";
    2.74 +Goal "0<k ==> (k*m < k*n) = (m<n)";
    2.75  by (dtac mult_less_cancel2 1);
    2.76  by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
    2.77  qed "mult_less_cancel1";
    2.78 @@ -579,7 +579,7 @@
    2.79  by (rtac Suc_mult_less_cancel1 1);
    2.80  qed "Suc_mult_le_cancel1";
    2.81  
    2.82 -Goal "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    2.83 +Goal "0<k ==> (m*k = n*k) = (m=n)";
    2.84  by (cut_facts_tac [less_linear] 1);
    2.85  by Safe_tac;
    2.86  by (assume_tac 2);
    2.87 @@ -587,7 +587,7 @@
    2.88  by (ALLGOALS Asm_full_simp_tac);
    2.89  qed "mult_cancel2";
    2.90  
    2.91 -Goal "!!k. 0<k ==> (k*m = k*n) = (m=n)";
    2.92 +Goal "0<k ==> (k*m = k*n) = (m=n)";
    2.93  by (dtac mult_cancel2 1);
    2.94  by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
    2.95  qed "mult_cancel1";
    2.96 @@ -601,7 +601,7 @@
    2.97  
    2.98  (** Lemma for gcd **)
    2.99  
   2.100 -Goal "!!m n. m = m*n ==> n=1 | m=0";
   2.101 +Goal "m = m*n ==> n=1 | m=0";
   2.102  by (dtac sym 1);
   2.103  by (rtac disjCI 1);
   2.104  by (rtac nat_less_cases 1 THEN assume_tac 2);
   2.105 @@ -626,11 +626,11 @@
   2.106  by (Asm_full_simp_tac 1);
   2.107  qed "add_less_imp_less_diff";
   2.108  
   2.109 -Goal "!! n. n <= m ==> Suc m - n = Suc (m - n)";
   2.110 +Goal "n <= m ==> Suc m - n = Suc (m - n)";
   2.111  by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
   2.112  qed "Suc_diff_le";
   2.113  
   2.114 -Goal "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
   2.115 +Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
   2.116  by (asm_full_simp_tac
   2.117      (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   2.118  qed "Suc_diff_Suc";
     3.1 --- a/src/HOL/Divides.ML	Tue Jul 14 13:33:12 1998 +0200
     3.2 +++ b/src/HOL/Divides.ML	Wed Jul 15 10:15:13 1998 +0200
     3.3 @@ -27,18 +27,18 @@
     3.4  by (simp_tac (simpset() addsimps [mod_def]) 1);
     3.5  qed "mod_eq";
     3.6  
     3.7 -Goal "!!m. m<n ==> m mod n = m";
     3.8 +Goal "m<n ==> m mod n = m";
     3.9  by (rtac (mod_eq RS wf_less_trans) 1);
    3.10  by (Asm_simp_tac 1);
    3.11  qed "mod_less";
    3.12  
    3.13 -Goal "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    3.14 +Goal "[| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    3.15  by (rtac (mod_eq RS wf_less_trans) 1);
    3.16  by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
    3.17  qed "mod_geq";
    3.18  
    3.19  (*NOT suitable for rewriting: loops*)
    3.20 -Goal "!!m. 0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
    3.21 +Goal "0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
    3.22  by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
    3.23  qed "mod_if";
    3.24  
    3.25 @@ -48,17 +48,17 @@
    3.26  qed "mod_1";
    3.27  Addsimps [mod_1];
    3.28  
    3.29 -Goal "!!n. 0<n ==> n mod n = 0";
    3.30 +Goal "0<n ==> n mod n = 0";
    3.31  by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
    3.32  qed "mod_self";
    3.33  
    3.34 -Goal "!!n. 0<n ==> (m+n) mod n = m mod n";
    3.35 +Goal "0<n ==> (m+n) mod n = m mod n";
    3.36  by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    3.37  by (stac (mod_geq RS sym) 2);
    3.38  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
    3.39  qed "mod_add_self2";
    3.40  
    3.41 -Goal "!!k. 0<n ==> (n+m) mod n = m mod n";
    3.42 +Goal "0<n ==> (n+m) mod n = m mod n";
    3.43  by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
    3.44  qed "mod_add_self1";
    3.45  
    3.46 @@ -67,13 +67,13 @@
    3.47  by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1]))));
    3.48  qed "mod_mult_self1";
    3.49  
    3.50 -Goal "!!m. 0<n ==> (m + n*k) mod n = m mod n";
    3.51 +Goal "0<n ==> (m + n*k) mod n = m mod n";
    3.52  by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
    3.53  qed "mod_mult_self2";
    3.54  
    3.55  Addsimps [mod_mult_self1, mod_mult_self2];
    3.56  
    3.57 -Goal "!!k. [| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
    3.58 +Goal "[| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
    3.59  by (res_inst_tac [("n","m")] less_induct 1);
    3.60  by (stac mod_if 1);
    3.61  by (Asm_simp_tac 1);
    3.62 @@ -81,7 +81,7 @@
    3.63  				      diff_less, diff_mult_distrib]) 1);
    3.64  qed "mod_mult_distrib";
    3.65  
    3.66 -Goal "!!k. [| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
    3.67 +Goal "[| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
    3.68  by (res_inst_tac [("n","m")] less_induct 1);
    3.69  by (stac mod_if 1);
    3.70  by (Asm_simp_tac 1);
    3.71 @@ -89,7 +89,7 @@
    3.72  				      diff_less, diff_mult_distrib2]) 1);
    3.73  qed "mod_mult_distrib2";
    3.74  
    3.75 -Goal "!!n. 0<n ==> m*n mod n = 0";
    3.76 +Goal "0<n ==> m*n mod n = 0";
    3.77  by (induct_tac "m" 1);
    3.78  by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
    3.79  by (dres_inst_tac [("m","m*n")] mod_add_self2 1);
    3.80 @@ -104,23 +104,23 @@
    3.81  by (simp_tac (simpset() addsimps [div_def]) 1);
    3.82  qed "div_eq";
    3.83  
    3.84 -Goal "!!m. m<n ==> m div n = 0";
    3.85 +Goal "m<n ==> m div n = 0";
    3.86  by (rtac (div_eq RS wf_less_trans) 1);
    3.87  by (Asm_simp_tac 1);
    3.88  qed "div_less";
    3.89  
    3.90 -Goal "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    3.91 +Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    3.92  by (rtac (div_eq RS wf_less_trans) 1);
    3.93  by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
    3.94  qed "div_geq";
    3.95  
    3.96  (*NOT suitable for rewriting: loops*)
    3.97 -Goal "!!m. 0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
    3.98 +Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
    3.99  by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
   3.100  qed "div_if";
   3.101  
   3.102  (*Main Result about quotient and remainder.*)
   3.103 -Goal "!!m. 0<n ==> (m div n)*n + m mod n = m";
   3.104 +Goal "0<n ==> (m div n)*n + m mod n = m";
   3.105  by (res_inst_tac [("n","m")] less_induct 1);
   3.106  by (stac mod_if 1);
   3.107  by (ALLGOALS (asm_simp_tac 
   3.108 @@ -130,7 +130,7 @@
   3.109  qed "mod_div_equality";
   3.110  
   3.111  (* a simple rearrangement of mod_div_equality: *)
   3.112 -Goal "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
   3.113 +Goal "0<k ==> k*(m div k) = m - (m mod k)";
   3.114  by (dres_inst_tac [("m","m")] mod_div_equality 1);
   3.115  by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
   3.116             K(IF_UNSOLVED no_tac)]);
   3.117 @@ -142,18 +142,18 @@
   3.118  qed "div_1";
   3.119  Addsimps [div_1];
   3.120  
   3.121 -Goal "!!n. 0<n ==> n div n = 1";
   3.122 +Goal "0<n ==> n div n = 1";
   3.123  by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
   3.124  qed "div_self";
   3.125  
   3.126  
   3.127 -Goal "!!n. 0<n ==> (m+n) div n = Suc (m div n)";
   3.128 +Goal "0<n ==> (m+n) div n = Suc (m div n)";
   3.129  by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
   3.130  by (stac (div_geq RS sym) 2);
   3.131  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
   3.132  qed "div_add_self2";
   3.133  
   3.134 -Goal "!!k. 0<n ==> (n+m) div n = Suc (m div n)";
   3.135 +Goal "0<n ==> (n+m) div n = Suc (m div n)";
   3.136  by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
   3.137  qed "div_add_self1";
   3.138  
   3.139 @@ -162,7 +162,7 @@
   3.140  by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1]))));
   3.141  qed "div_mult_self1";
   3.142  
   3.143 -Goal "!!m. 0<n ==> (m + n*k) div n = k + m div n";
   3.144 +Goal "0<n ==> (m + n*k) div n = k + m div n";
   3.145  by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
   3.146  qed "div_mult_self2";
   3.147  
   3.148 @@ -170,10 +170,10 @@
   3.149  
   3.150  
   3.151  (* Monotonicity of div in first argument *)
   3.152 -Goal "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
   3.153 +Goal "0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
   3.154  by (res_inst_tac [("n","n")] less_induct 1);
   3.155  by (Clarify_tac 1);
   3.156 -by (case_tac "na<k" 1);
   3.157 +by (case_tac "n<k" 1);
   3.158  (* 1  case n<k *)
   3.159  by (subgoal_tac "m<k" 1);
   3.160  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
   3.161 @@ -188,7 +188,7 @@
   3.162  
   3.163  
   3.164  (* Antimonotonicity of div in second argument *)
   3.165 -Goal "!!k m n. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
   3.166 +Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
   3.167  by (subgoal_tac "0<n" 1);
   3.168   by (trans_tac 2);
   3.169  by (res_inst_tac [("n","k")] less_induct 1);
   3.170 @@ -205,7 +205,7 @@
   3.171  by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
   3.172  qed "div_le_mono2";
   3.173  
   3.174 -Goal "!!m n. 0<n ==> m div n <= m";
   3.175 +Goal "0<n ==> m div n <= m";
   3.176  by (subgoal_tac "m div n <= m div 1" 1);
   3.177  by (Asm_full_simp_tac 1);
   3.178  by (rtac div_le_mono2 1);
   3.179 @@ -214,7 +214,7 @@
   3.180  Addsimps [div_le_dividend];
   3.181  
   3.182  (* Similar for "less than" *)
   3.183 -Goal "!!m n. 1<n ==> (0 < m) --> (m div n < m)";
   3.184 +Goal "1<n ==> (0 < m) --> (m div n < m)";
   3.185  by (res_inst_tac [("n","m")] less_induct 1);
   3.186  by (Simp_tac 1);
   3.187  by (rename_tac "m" 1);
   3.188 @@ -255,7 +255,7 @@
   3.189  by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
   3.190  qed "mod_Suc";
   3.191  
   3.192 -Goal "!!m n. 0<n ==> m mod n < n";
   3.193 +Goal "0<n ==> m mod n < n";
   3.194  by (res_inst_tac [("n","m")] less_induct 1);
   3.195  by (excluded_middle_tac "na<n" 1);
   3.196  (*case na<n*)
   3.197 @@ -270,7 +270,7 @@
   3.198  (*With less_zeroE, causes case analysis on b<2*)
   3.199  AddSEs [less_SucE];
   3.200  
   3.201 -Goal "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   3.202 +Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
   3.203  by (subgoal_tac "k mod 2 < 2" 1);
   3.204  by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
   3.205  by (Asm_simp_tac 1);
   3.206 @@ -311,7 +311,7 @@
   3.207  
   3.208  (*** More division laws ***)
   3.209  
   3.210 -Goal "!!n. 0<n ==> m*n div n = m";
   3.211 +Goal "0<n ==> m*n div n = m";
   3.212  by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
   3.213  by (assume_tac 1);
   3.214  by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
   3.215 @@ -319,7 +319,7 @@
   3.216  Addsimps [div_mult_self_is_m];
   3.217  
   3.218  (*Cancellation law for division*)
   3.219 -Goal "!!k. [| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   3.220 +Goal "[| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
   3.221  by (res_inst_tac [("n","m")] less_induct 1);
   3.222  by (case_tac "na<n" 1);
   3.223  by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
   3.224 @@ -333,7 +333,7 @@
   3.225  qed "div_cancel";
   3.226  Addsimps [div_cancel];
   3.227  
   3.228 -Goal "!!k. [| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   3.229 +Goal "[| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
   3.230  by (res_inst_tac [("n","m")] less_induct 1);
   3.231  by (case_tac "na<n" 1);
   3.232  by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
   3.233 @@ -356,7 +356,7 @@
   3.234  qed "dvd_0_right";
   3.235  Addsimps [dvd_0_right];
   3.236  
   3.237 -Goalw [dvd_def] "!!m. 0 dvd m ==> m = 0";
   3.238 +Goalw [dvd_def] "0 dvd m ==> m = 0";
   3.239  by (fast_tac (claset() addss simpset()) 1);
   3.240  qed "dvd_0_left";
   3.241  
   3.242 @@ -370,33 +370,33 @@
   3.243  qed "dvd_refl";
   3.244  Addsimps [dvd_refl];
   3.245  
   3.246 -Goalw [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
   3.247 +Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
   3.248  by (blast_tac (claset() addIs [mult_assoc] ) 1);
   3.249  qed "dvd_trans";
   3.250  
   3.251 -Goalw [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
   3.252 +Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
   3.253  by (fast_tac (claset() addDs [mult_eq_self_implies_10]
   3.254                       addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
   3.255  qed "dvd_anti_sym";
   3.256  
   3.257 -Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
   3.258 +Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
   3.259  by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
   3.260  qed "dvd_add";
   3.261  
   3.262 -Goalw [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m-n)";
   3.263 +Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
   3.264  by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
   3.265  qed "dvd_diff";
   3.266  
   3.267 -Goal "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
   3.268 +Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
   3.269  by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
   3.270  by (blast_tac (claset() addIs [dvd_add]) 1);
   3.271  qed "dvd_diffD";
   3.272  
   3.273 -Goalw [dvd_def] "!!k. k dvd n ==> k dvd (m*n)";
   3.274 +Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
   3.275  by (blast_tac (claset() addIs [mult_left_commute]) 1);
   3.276  qed "dvd_mult";
   3.277  
   3.278 -Goal "!!k. k dvd m ==> k dvd (m*n)";
   3.279 +Goal "k dvd m ==> k dvd (m*n)";
   3.280  by (stac mult_commute 1);
   3.281  by (etac dvd_mult 1);
   3.282  qed "dvd_mult2";
   3.283 @@ -404,7 +404,7 @@
   3.284  (* k dvd (m*k) *)
   3.285  AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   3.286  
   3.287 -Goalw [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   3.288 +Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
   3.289  by (Clarify_tac 1);
   3.290  by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
   3.291  by (res_inst_tac 
   3.292 @@ -414,30 +414,30 @@
   3.293                                       mult_mod_distrib, add_mult_distrib2]) 1);
   3.294  qed "dvd_mod";
   3.295  
   3.296 -Goal "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
   3.297 +Goal "[| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
   3.298  by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
   3.299  by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
   3.300  by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
   3.301  qed "dvd_mod_imp_dvd";
   3.302  
   3.303 -Goalw [dvd_def]  "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
   3.304 +Goalw [dvd_def]  "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
   3.305  by (etac exE 1);
   3.306  by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
   3.307  by (Blast_tac 1);
   3.308  qed "dvd_mult_cancel";
   3.309  
   3.310 -Goalw [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
   3.311 +Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
   3.312  by (Clarify_tac 1);
   3.313  by (res_inst_tac [("x","k*ka")] exI 1);
   3.314  by (asm_simp_tac (simpset() addsimps mult_ac) 1);
   3.315  qed "mult_dvd_mono";
   3.316  
   3.317 -Goalw [dvd_def] "!!c. (i*j) dvd k ==> i dvd k";
   3.318 +Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
   3.319  by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
   3.320  by (Blast_tac 1);
   3.321  qed "dvd_mult_left";
   3.322  
   3.323 -Goalw [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
   3.324 +Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
   3.325  by (Clarify_tac 1);
   3.326  by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
   3.327  by (etac conjE 1);
   3.328 @@ -447,11 +447,11 @@
   3.329  by (Simp_tac 1);
   3.330  qed "dvd_imp_le";
   3.331  
   3.332 -Goalw [dvd_def] "!!k. 0<k ==> (k dvd n) = (n mod k = 0)";
   3.333 +Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)";
   3.334  by Safe_tac;
   3.335 +by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   3.336 +by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
   3.337  by (stac mult_commute 1);
   3.338  by (Asm_simp_tac 1);
   3.339 -by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
   3.340 -by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   3.341  by (Blast_tac 1);
   3.342  qed "dvd_eq_mod_eq_0";
     4.1 --- a/src/HOL/Finite.ML	Tue Jul 14 13:33:12 1998 +0200
     4.2 +++ b/src/HOL/Finite.ML	Wed Jul 15 10:15:13 1998 +0200
     4.3 @@ -42,7 +42,7 @@
     4.4  qed "finite_UnI";
     4.5  
     4.6  (*Every subset of a finite set is finite*)
     4.7 -Goal "!!B. finite B ==> ALL A. A<=B --> finite A";
     4.8 +Goal "finite B ==> ALL A. A<=B --> finite A";
     4.9  by (etac finite_induct 1);
    4.10  by (Simp_tac 1);
    4.11  by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
    4.12 @@ -50,7 +50,7 @@
    4.13  by (ALLGOALS Asm_simp_tac);
    4.14  val lemma = result();
    4.15  
    4.16 -Goal "!!A. [| A<=B;  finite B |] ==> finite A";
    4.17 +Goal "[| A<=B;  finite B |] ==> finite A";
    4.18  by (dtac lemma 1);
    4.19  by (Blast_tac 1);
    4.20  qed "finite_subset";
    4.21 @@ -70,7 +70,7 @@
    4.22  Addsimps[finite_insert];
    4.23  
    4.24  (*The image of a finite set is finite *)
    4.25 -Goal  "!!F. finite F ==> finite(h``F)";
    4.26 +Goal  "finite F ==> finite(h``F)";
    4.27  by (etac finite_induct 1);
    4.28  by (Simp_tac 1);
    4.29  by (Asm_simp_tac 1);
    4.30 @@ -111,7 +111,7 @@
    4.31  AddIffs [finite_Diff_singleton];
    4.32  
    4.33  (*Lemma for proving finite_imageD*)
    4.34 -Goal "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A";
    4.35 +Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A";
    4.36  by (etac finite_induct 1);
    4.37   by (ALLGOALS Asm_simp_tac);
    4.38  by (Clarify_tac 1);
    4.39 @@ -127,7 +127,7 @@
    4.40      (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
    4.41  val lemma = result();
    4.42  
    4.43 -Goal "!!A. [| finite(f``A);  inj_on f A |] ==> finite A";
    4.44 +Goal "[| finite(f``A);  inj_on f A |] ==> finite A";
    4.45  by (dtac lemma 1);
    4.46  by (Blast_tac 1);
    4.47  qed "finite_imageD";
    4.48 @@ -151,7 +151,7 @@
    4.49  
    4.50  (** The powerset of a finite set **)
    4.51  
    4.52 -Goal "!!A. finite(Pow A) ==> finite A";
    4.53 +Goal "finite(Pow A) ==> finite A";
    4.54  by (subgoal_tac "finite ((%x.{x})``A)" 1);
    4.55  by (rtac finite_subset 2);
    4.56  by (assume_tac 3);
    4.57 @@ -273,7 +273,7 @@
    4.58  by (Blast_tac 1);
    4.59  val lemma = result();
    4.60  
    4.61 -Goal "!!A. [| finite A; x ~: A |] ==> \
    4.62 +Goal "[| finite A; x ~: A |] ==> \
    4.63  \ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
    4.64  by (rtac Least_equality 1);
    4.65   by (dtac finite_has_card 1);
    4.66 @@ -309,12 +309,12 @@
    4.67  qed "card_insert_disjoint";
    4.68  Addsimps [card_insert_disjoint];
    4.69  
    4.70 -Goal "!!A. finite A ==> card A <= card (insert x A)";
    4.71 +Goal "finite A ==> card A <= card (insert x A)";
    4.72  by (case_tac "x: A" 1);
    4.73  by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
    4.74  qed "card_insert_le";
    4.75  
    4.76 -Goal  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
    4.77 +Goal  "finite A ==> !B. B <= A --> card(B) <= card(A)";
    4.78  by (etac finite_induct 1);
    4.79  by (Simp_tac 1);
    4.80  by (Clarify_tac 1);
    4.81 @@ -325,13 +325,13 @@
    4.82  	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
    4.83  qed_spec_mp "card_mono";
    4.84  
    4.85 -Goal "!!A B. [| finite A; finite B |]\
    4.86 +Goal "[| finite A; finite B |]\
    4.87  \                       ==> A Int B = {} --> card(A Un B) = card A + card B";
    4.88  by (etac finite_induct 1);
    4.89  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
    4.90  qed_spec_mp "card_Un_disjoint";
    4.91  
    4.92 -Goal "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
    4.93 +Goal "[| finite A; B<=A |] ==> card A - card B = card (A - B)";
    4.94  by (subgoal_tac "(A-B) Un B = A" 1);
    4.95  by (Blast_tac 2);
    4.96  by (rtac (add_right_cancel RS iffD1) 1);
    4.97 @@ -344,18 +344,18 @@
    4.98  			 add_diff_inverse, card_mono, finite_subset])));
    4.99  qed "card_Diff_subset";
   4.100  
   4.101 -Goal "!!A. [| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
   4.102 +Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A";
   4.103  by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1);
   4.104  by (assume_tac 1);
   4.105  by (Asm_simp_tac 1);
   4.106  qed "card_Suc_Diff";
   4.107  
   4.108 -Goal "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
   4.109 +Goal "[| finite A; x: A |] ==> card(A-{x}) < card A";
   4.110  by (rtac Suc_less_SucD 1);
   4.111  by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
   4.112  qed "card_Diff";
   4.113  
   4.114 -Goal "!!A. finite A ==> card(A-{x}) <= card A";
   4.115 +Goal "finite A ==> card(A-{x}) <= card A";
   4.116  by (case_tac "x: A" 1);
   4.117  by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le])));
   4.118  qed "card_Diff_le";
   4.119 @@ -363,14 +363,14 @@
   4.120  
   4.121  (*** Cardinality of the Powerset ***)
   4.122  
   4.123 -Goal "!!A. finite A ==> card(insert x A) = Suc(card(A-{x}))";
   4.124 +Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))";
   4.125  by (case_tac "x:A" 1);
   4.126  by (ALLGOALS 
   4.127      (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb])));
   4.128  qed "card_insert";
   4.129  Addsimps [card_insert];
   4.130  
   4.131 -Goal "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A";
   4.132 +Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A";
   4.133  by (etac finite_induct 1);
   4.134  by (ALLGOALS Asm_simp_tac);
   4.135  by Safe_tac;
   4.136 @@ -382,7 +382,7 @@
   4.137  by (Blast_tac 1);
   4.138  qed_spec_mp "card_image";
   4.139  
   4.140 -Goal "!!A. finite A ==> card (Pow A) = 2 ^ card A";
   4.141 +Goal "finite A ==> card (Pow A) = 2 ^ card A";
   4.142  by (etac finite_induct 1);
   4.143  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
   4.144  by (stac card_Un_disjoint 1);
   4.145 @@ -418,7 +418,7 @@
   4.146  
   4.147  (*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.
   4.148    The "finite C" premise is redundant*)
   4.149 -Goal "!!C. finite C ==> finite (Union C) --> \
   4.150 +Goal "finite C ==> finite (Union C) --> \
   4.151  \          (! c : C. k dvd card c) -->  \
   4.152  \          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
   4.153  \          --> k dvd card(Union C)";
     5.1 --- a/src/HOL/Fun.ML	Tue Jul 14 13:33:12 1998 +0200
     5.2 +++ b/src/HOL/Fun.ML	Wed Jul 15 10:15:13 1998 +0200
     5.3 @@ -97,7 +97,7 @@
     5.4  by (REPEAT (resolve_tac prems 1));
     5.5  qed "inj_onD";
     5.6  
     5.7 -Goal "!!x y.[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
     5.8 +Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
     5.9  by (blast_tac (claset() addSDs [inj_onD]) 1);
    5.10  qed "inj_on_iff";
    5.11  
    5.12 @@ -135,7 +135,7 @@
    5.13  by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
    5.14  qed "inv_injective";
    5.15  
    5.16 -Goal "!!f. [| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
    5.17 +Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
    5.18  by (fast_tac (claset() addIs [inj_onI] 
    5.19                        addEs [inv_injective,injD]) 1);
    5.20  qed "inj_on_inv";
    5.21 @@ -150,11 +150,11 @@
    5.22  by (Blast_tac 1);
    5.23  qed "inj_on_image_set_diff";
    5.24  
    5.25 -Goalw [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
    5.26 +Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B";
    5.27  by (Blast_tac 1);
    5.28  qed "image_Int";
    5.29  
    5.30 -Goalw [inj_def] "!!f. inj f ==> f``(A-B) = f``A - f``B";
    5.31 +Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B";
    5.32  by (Blast_tac 1);
    5.33  qed "image_set_diff";
    5.34  
     6.1 --- a/src/HOL/IOA/Asig.ML	Tue Jul 14 13:33:12 1998 +0200
     6.2 +++ b/src/HOL/IOA/Asig.ML	Wed Jul 15 10:15:13 1998 +0200
     6.3 @@ -10,10 +10,10 @@
     6.4  
     6.5  val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
     6.6  
     6.7 -Goal "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
     6.8 +Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
     6.9  by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    6.10  qed"int_and_ext_is_act";
    6.11  
    6.12 -Goal "!!a.[|a:externals(S)|] ==> a:actions(S)";
    6.13 +Goal "[|a:externals(S)|] ==> a:actions(S)";
    6.14  by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    6.15  qed"ext_is_act";
     7.1 --- a/src/HOL/IOA/IOA.ML	Tue Jul 14 13:33:12 1998 +0200
     7.2 +++ b/src/HOL/IOA/IOA.ML	Wed Jul 15 10:15:13 1998 +0200
     7.3 @@ -46,7 +46,7 @@
     7.4    by (Fast_tac 1);
     7.5  qed "mk_trace_thm";
     7.6  
     7.7 -Goalw [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
     7.8 +Goalw [reachable_def] "s:starts_of(A) ==> reachable A s";
     7.9    by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1);
    7.10    by (Simp_tac 1);
    7.11    by (asm_simp_tac (simpset() addsimps exec_rws) 1);
     8.1 --- a/src/HOL/IOA/Solve.ML	Tue Jul 14 13:33:12 1998 +0200
     8.2 +++ b/src/HOL/IOA/Solve.ML	Wed Jul 15 10:15:13 1998 +0200
     8.3 @@ -65,7 +65,7 @@
     8.4   by (Fast_tac 1);
     8.5  val externals_of_par_extra = result(); 
     8.6  
     8.7 -Goal "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
     8.8 +Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
     8.9  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    8.10  by (etac bexE 1);
    8.11  by (res_inst_tac [("x",
    8.12 @@ -85,7 +85,7 @@
    8.13  
    8.14  (* Exact copy of proof of comp1_reachable for the second 
    8.15     component of a parallel composition.     *)
    8.16 -Goal "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    8.17 +Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)";
    8.18  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    8.19  by (etac bexE 1);
    8.20  by (res_inst_tac [("x",
    8.21 @@ -105,7 +105,7 @@
    8.22  Delsplits [split_if];
    8.23  
    8.24  (* Composition of possibility-mappings *)
    8.25 -Goalw [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
    8.26 +Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
    8.27  \               externals(asig_of(A1))=externals(asig_of(C1)) &\
    8.28  \               is_weak_pmap g C2 A2 &  \
    8.29  \               externals(asig_of(A2))=externals(asig_of(C2)) & \
    8.30 @@ -149,7 +149,7 @@
    8.31  qed"fxg_is_weak_pmap_of_product_IOA";
    8.32  
    8.33  
    8.34 -Goal "!!s.[| reachable (rename C g) s |] ==> reachable C s";
    8.35 +Goal "[| reachable (rename C g) s |] ==> reachable C s";
    8.36  by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 
    8.37  by (etac bexE 1);
    8.38  by (res_inst_tac [("x",
    8.39 @@ -166,7 +166,7 @@
    8.40  qed"reachable_rename_ioa";
    8.41  
    8.42  
    8.43 -Goal "!!f.[| is_weak_pmap f C A |]\
    8.44 +Goal "[| is_weak_pmap f C A |]\
    8.45  \                      ==> (is_weak_pmap f (rename C g) (rename A g))";
    8.46  by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1);
    8.47  by (rtac conjI 1);
     9.1 --- a/src/HOL/Induct/Acc.ML	Tue Jul 14 13:33:12 1998 +0200
     9.2 +++ b/src/HOL/Induct/Acc.ML	Wed Jul 15 10:15:13 1998 +0200
     9.3 @@ -18,7 +18,7 @@
     9.4                              map (rewrite_rule [pred_def]) acc.intrs)) 1);
     9.5  qed "accI";
     9.6  
     9.7 -Goal "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
     9.8 +Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
     9.9  by (etac acc.elim 1);
    9.10  by (rewtac pred_def);
    9.11  by (Fast_tac 1);
    10.1 --- a/src/HOL/Induct/Com.ML	Tue Jul 14 13:33:12 1998 +0200
    10.2 +++ b/src/HOL/Induct/Com.ML	Wed Jul 15 10:15:13 1998 +0200
    10.3 @@ -19,7 +19,7 @@
    10.4  AddSEs exec_elim_cases;
    10.5  
    10.6  (*This theorem justifies using "exec" in the inductive definition of "eval"*)
    10.7 -Goalw exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
    10.8 +Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
    10.9  by (rtac lfp_mono 1);
   10.10  by (REPEAT (ares_tac basic_monos 1));
   10.11  qed "exec_mono";
   10.12 @@ -29,7 +29,7 @@
   10.13  Unify.search_bound := 60;
   10.14  
   10.15  (*Command execution is functional (deterministic) provided evaluation is*)
   10.16 -Goal "!!x. Function ev ==> Function(exec ev)";
   10.17 +Goal "Function ev ==> Function(exec ev)";
   10.18  by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
   10.19  by (REPEAT (rtac allI 1));
   10.20  by (rtac impI 1);
   10.21 @@ -48,7 +48,7 @@
   10.22  by (Simp_tac 1);
   10.23  qed "assign_same";
   10.24  
   10.25 -Goalw [assign_def] "!!y. y~=x ==> (s[v/x])y = s y";
   10.26 +Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
   10.27  by (Asm_simp_tac 1);
   10.28  qed "assign_different";
   10.29  
    11.1 --- a/src/HOL/Induct/Comb.ML	Tue Jul 14 13:33:12 1998 +0200
    11.2 +++ b/src/HOL/Induct/Comb.ML	Wed Jul 15 10:15:13 1998 +0200
    11.3 @@ -55,22 +55,22 @@
    11.4  AddIs  [contract.Ap1, contract.Ap2];
    11.5  AddSEs [K_contractE, S_contractE, Ap_contractE];
    11.6  
    11.7 -Goalw [I_def] "!!z. I -1-> z ==> P";
    11.8 +Goalw [I_def] "I -1-> z ==> P";
    11.9  by (Blast_tac 1);
   11.10  qed "I_contract_E";
   11.11  AddSEs [I_contract_E];
   11.12  
   11.13 -Goal "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
   11.14 +Goal "K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
   11.15  by (Blast_tac 1);
   11.16  qed "K1_contractD";
   11.17  AddSEs [K1_contractD];
   11.18  
   11.19 -Goal "!!x z. x ---> y ==> x#z ---> y#z";
   11.20 +Goal "x ---> y ==> x#z ---> y#z";
   11.21  by (etac rtrancl_induct 1);
   11.22  by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
   11.23  qed "Ap_reduce1";
   11.24  
   11.25 -Goal "!!x z. x ---> y ==> z#x ---> z#y";
   11.26 +Goal "x ---> y ==> z#x ---> z#y";
   11.27  by (etac rtrancl_induct 1);
   11.28  by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
   11.29  qed "Ap_reduce2";
   11.30 @@ -108,12 +108,12 @@
   11.31  
   11.32  (*** Basic properties of parallel contraction ***)
   11.33  
   11.34 -Goal "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
   11.35 +Goal "K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
   11.36  by (Blast_tac 1);
   11.37  qed "K1_parcontractD";
   11.38  AddSDs [K1_parcontractD];
   11.39  
   11.40 -Goal "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
   11.41 +Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
   11.42  by (Blast_tac 1);
   11.43  qed "S1_parcontractD";
   11.44  AddSDs [S1_parcontractD];
    12.1 --- a/src/HOL/Induct/Exp.ML	Tue Jul 14 13:33:12 1998 +0200
    12.2 +++ b/src/HOL/Induct/Exp.ML	Wed Jul 15 10:15:13 1998 +0200
    12.3 @@ -97,7 +97,7 @@
    12.4  qed "Function_eval";
    12.5  
    12.6  
    12.7 -Goal "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
    12.8 +Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
    12.9  by (etac eval_induct 1);
   12.10  by (ALLGOALS Asm_simp_tac);
   12.11  val lemma = result();
   12.12 @@ -107,7 +107,7 @@
   12.13  
   12.14  
   12.15  (*This theorem says that "WHILE TRUE DO c" cannot terminate*)
   12.16 -Goal "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
   12.17 +Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
   12.18  by (etac exec.induct 1);
   12.19  by Auto_tac;
   12.20  bind_thm ("while_true_E", refl RSN (2, result() RS mp));
   12.21 @@ -115,7 +115,7 @@
   12.22  
   12.23  (** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  WHILE e DO c **)
   12.24  
   12.25 -Goal "!!x. (c',s) -[eval]-> t ==> \
   12.26 +Goal "(c',s) -[eval]-> t ==> \
   12.27  \              (c' = WHILE e DO c) --> \
   12.28  \              (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
   12.29  by (etac exec.induct 1);
   12.30 @@ -124,7 +124,7 @@
   12.31  bind_thm ("while_if1", refl RSN (2, result() RS mp));
   12.32  
   12.33  
   12.34 -Goal "!!x. (c',s) -[eval]-> t ==> \
   12.35 +Goal "(c',s) -[eval]-> t ==> \
   12.36  \              (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
   12.37  \              (WHILE e DO c, s) -[eval]-> t";
   12.38  by (etac exec.induct 1);
   12.39 @@ -143,7 +143,7 @@
   12.40  (** Equivalence of  (IF e THEN c1 ELSE c2);;c
   12.41                 and  IF e THEN (c1;;c) ELSE (c2;;c)   **)
   12.42  
   12.43 -Goal "!!x. (c',s) -[eval]-> t ==> \
   12.44 +Goal "(c',s) -[eval]-> t ==> \
   12.45  \              (c' = (IF e THEN c1 ELSE c2);;c) --> \
   12.46  \              (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
   12.47  by (etac exec.induct 1);
   12.48 @@ -152,7 +152,7 @@
   12.49  bind_thm ("if_semi1", refl RSN (2, result() RS mp));
   12.50  
   12.51  
   12.52 -Goal "!!x. (c',s) -[eval]-> t ==> \
   12.53 +Goal "(c',s) -[eval]-> t ==> \
   12.54  \              (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
   12.55  \              ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
   12.56  by (etac exec.induct 1);
   12.57 @@ -172,7 +172,7 @@
   12.58                 and  VALOF c1;;c2 RESULTIS e
   12.59   **)
   12.60  
   12.61 -Goal "!!x. (e',s) -|-> (v,s') ==> \
   12.62 +Goal "(e',s) -|-> (v,s') ==> \
   12.63  \              (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
   12.64  \              (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
   12.65  by (etac eval_induct 1);
   12.66 @@ -181,7 +181,7 @@
   12.67  bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
   12.68  
   12.69  
   12.70 -Goal "!!x. (e',s) -|-> (v,s') ==> \
   12.71 +Goal "(e',s) -|-> (v,s') ==> \
   12.72  \              (e' = VALOF c1;;c2 RESULTIS e) --> \
   12.73  \              (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
   12.74  by (etac eval_induct 1);
   12.75 @@ -198,7 +198,7 @@
   12.76  
   12.77  (** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
   12.78  
   12.79 -Goal "!!x. (e',s) -|-> (v,s') ==> \
   12.80 +Goal "(e',s) -|-> (v,s') ==> \
   12.81  \              (e' = VALOF SKIP RESULTIS e) --> \
   12.82  \              (e, s) -|-> (v,s')";
   12.83  by (etac eval_induct 1);
   12.84 @@ -206,7 +206,7 @@
   12.85  by (Blast_tac 1); 
   12.86  bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
   12.87  
   12.88 -Goal "!!x. (e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
   12.89 +Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
   12.90  by (Blast_tac 1);
   12.91  qed "valof_skip2";
   12.92  
   12.93 @@ -217,7 +217,7 @@
   12.94  
   12.95  (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
   12.96  
   12.97 -Goal "!!x. (e',s) -|-> (v,s'') ==> \
   12.98 +Goal "(e',s) -|-> (v,s'') ==> \
   12.99  \              (e' = VALOF x:=e RESULTIS X x) --> \
  12.100  \              (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
  12.101  by (etac eval_induct 1);
  12.102 @@ -229,7 +229,7 @@
  12.103  bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
  12.104  
  12.105  
  12.106 -Goal "!!x. (e,s) -|-> (v,s') ==> \
  12.107 +Goal "(e,s) -|-> (v,s') ==> \
  12.108  \              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
  12.109  by (Blast_tac 1);
  12.110  qed "valof_assign2";
    13.1 --- a/src/HOL/Induct/LFilter.ML	Tue Jul 14 13:33:12 1998 +0200
    13.2 +++ b/src/HOL/Induct/LFilter.ML	Wed Jul 15 10:15:13 1998 +0200
    13.3 @@ -18,19 +18,19 @@
    13.4  AddSEs [findRel_LConsE];
    13.5  
    13.6  
    13.7 -Goal "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
    13.8 +Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
    13.9  by (etac findRel.induct 1);
   13.10  by (Blast_tac 1);
   13.11  by (Blast_tac 1);
   13.12  qed_spec_mp "findRel_functional";
   13.13  
   13.14 -Goal "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
   13.15 +Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
   13.16  by (etac findRel.induct 1);
   13.17  by (Blast_tac 1);
   13.18  by (Blast_tac 1);
   13.19  qed_spec_mp "findRel_imp_LCons";
   13.20  
   13.21 -Goal "!!p. (LNil,l): findRel p ==> R";
   13.22 +Goal "(LNil,l): findRel p ==> R";
   13.23  by (blast_tac (claset() addEs [findRel.elim]) 1);
   13.24  qed "findRel_LNil";
   13.25  
   13.26 @@ -39,7 +39,7 @@
   13.27  
   13.28  (*** Properties of Domain (findRel p) ***)
   13.29  
   13.30 -Goal "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
   13.31 +Goal "LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
   13.32  by (case_tac "p x" 1);
   13.33  by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
   13.34  qed "LCons_Domain_findRel";
   13.35 @@ -73,22 +73,22 @@
   13.36  qed "find_LNil";
   13.37  Addsimps [find_LNil];
   13.38  
   13.39 -Goalw [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
   13.40 +Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
   13.41  by (blast_tac (claset() addDs [findRel_functional]) 1);
   13.42  qed "findRel_imp_find";
   13.43  Addsimps [findRel_imp_find];
   13.44  
   13.45 -Goal "!!p. p x ==> find p (LCons x l) = LCons x l";
   13.46 +Goal "p x ==> find p (LCons x l) = LCons x l";
   13.47  by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
   13.48  qed "find_LCons_found";
   13.49  Addsimps [find_LCons_found];
   13.50  
   13.51 -Goalw [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
   13.52 +Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
   13.53  by (Blast_tac 1);
   13.54  qed "diverge_find_LNil";
   13.55  Addsimps [diverge_find_LNil];
   13.56  
   13.57 -Goal "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
   13.58 +Goal "~ (p x) ==> find p (LCons x l) = find p l";
   13.59  by (case_tac "LCons x l : Domain(findRel p)" 1);
   13.60  by (Asm_full_simp_tac 2);
   13.61  by (Clarify_tac 1);
   13.62 @@ -111,7 +111,7 @@
   13.63  qed "lfilter_LNil";
   13.64  Addsimps [lfilter_LNil];
   13.65  
   13.66 -Goal "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
   13.67 +Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil";
   13.68  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   13.69  by (Asm_simp_tac 1);
   13.70  qed "diverge_lfilter_LNil";
   13.71 @@ -119,7 +119,7 @@
   13.72  Addsimps [diverge_lfilter_LNil];
   13.73  
   13.74  
   13.75 -Goal "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
   13.76 +Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
   13.77  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   13.78  by (Asm_simp_tac 1);
   13.79  qed "lfilter_LCons_found";
   13.80 @@ -127,7 +127,7 @@
   13.81    subsumes both*)
   13.82  
   13.83  
   13.84 -Goal "!!p. (l, LCons x l') : findRel p \
   13.85 +Goal "(l, LCons x l') : findRel p \
   13.86  \              ==> lfilter p l = LCons x (lfilter p l')";
   13.87  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   13.88  by (Asm_simp_tac 1);
   13.89 @@ -136,7 +136,7 @@
   13.90  Addsimps [findRel_imp_lfilter];
   13.91  
   13.92  
   13.93 -Goal "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
   13.94 +Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
   13.95  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   13.96  by (case_tac "LCons x l : Domain(findRel p)" 1);
   13.97  by (Asm_full_simp_tac 2);
   13.98 @@ -155,7 +155,7 @@
   13.99  Addsimps [lfilter_LCons];
  13.100  
  13.101  
  13.102 -Goal "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
  13.103 +Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)";
  13.104  by (rtac notI 1);
  13.105  by (etac Domain_findRelE 1);
  13.106  by (etac rev_mp 1);
  13.107 @@ -163,7 +163,7 @@
  13.108  qed "lfilter_eq_LNil";
  13.109  
  13.110  
  13.111 -Goal "!!p. lfilter p l = LCons x l' -->     \
  13.112 +Goal "lfilter p l = LCons x l' -->     \
  13.113  \              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
  13.114  by (stac (lfilter_def RS def_llist_corec) 1);
  13.115  by (case_tac "l : Domain(findRel p)" 1);
  13.116 @@ -205,7 +205,7 @@
  13.117       lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
  13.118   ***)
  13.119  
  13.120 -Goal "!!p. (l,l') : findRel q \
  13.121 +Goal "(l,l') : findRel q \
  13.122  \           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
  13.123  by (etac findRel.induct 1);
  13.124  by (blast_tac (claset() addIs findRel.intrs) 1);
  13.125 @@ -214,7 +214,7 @@
  13.126  
  13.127  val findRel_conj = refl RSN (2, findRel_conj_lemma);
  13.128  
  13.129 -Goal "!!p. (l,l'') : findRel (%x. p x & q x) \
  13.130 +Goal "(l,l'') : findRel (%x. p x & q x) \
  13.131  \              ==> (l, LCons x l') : findRel q --> ~ p x     \
  13.132  \                  --> l' : Domain (findRel (%x. p x & q x))";
  13.133  by (etac findRel.induct 1);
  13.134 @@ -222,7 +222,7 @@
  13.135  qed_spec_mp "findRel_not_conj_Domain";
  13.136  
  13.137  
  13.138 -Goal "!!p. (l,lxx) : findRel q ==> \
  13.139 +Goal "(l,lxx) : findRel q ==> \
  13.140  \            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
  13.141  \            --> (l,lz) : findRel (%x. p x & q x)";
  13.142  by (etac findRel.induct 1);
  13.143 @@ -230,7 +230,7 @@
  13.144  qed_spec_mp "findRel_conj2";
  13.145  
  13.146  
  13.147 -Goal "!!p. (lx,ly) : findRel p \
  13.148 +Goal "(lx,ly) : findRel p \
  13.149  \              ==> ALL l. lx = lfilter q l \
  13.150  \                  --> l : Domain (findRel(%x. p x & q x))";
  13.151  by (etac findRel.induct 1);
  13.152 @@ -245,7 +245,7 @@
  13.153  qed_spec_mp "findRel_lfilter_Domain_conj";
  13.154  
  13.155  
  13.156 -Goal "!!p. (l,l'') : findRel(%x. p x & q x) \
  13.157 +Goal "(l,l'') : findRel(%x. p x & q x) \
  13.158  \              ==> l'' = LCons y l' --> \
  13.159  \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
  13.160  by (etac findRel.induct 1);
  13.161 @@ -299,13 +299,13 @@
  13.162       lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
  13.163   ***)
  13.164  
  13.165 -Goal "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
  13.166 +Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
  13.167  by (etac findRel.induct 1);
  13.168  by (ALLGOALS Asm_full_simp_tac);
  13.169  qed "findRel_lmap_Domain";
  13.170  
  13.171  
  13.172 -Goal "!!p. lmap f l = LCons x l' -->     \
  13.173 +Goal "lmap f l = LCons x l' -->     \
  13.174  \              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
  13.175  by (stac (lmap_def RS def_llist_corec) 1);
  13.176  by (res_inst_tac [("l", "l")] llistE 1);
  13.177 @@ -313,7 +313,7 @@
  13.178  qed_spec_mp "lmap_eq_LCons";
  13.179  
  13.180  
  13.181 -Goal "!!p. (lx,ly) : findRel p ==>  \
  13.182 +Goal "(lx,ly) : findRel p ==>  \
  13.183  \    ALL l. lmap f l = lx --> ly = LCons x l' --> \
  13.184  \    (EX y l''. x = f y & l' = lmap f l'' &       \
  13.185  \    (l, LCons y l'') : findRel(%x. p(f x)))";
    14.1 --- a/src/HOL/Induct/LList.ML	Tue Jul 14 13:33:12 1998 +0200
    14.2 +++ b/src/HOL/Induct/LList.ML	Wed Jul 15 10:15:13 1998 +0200
    14.3 @@ -13,7 +13,7 @@
    14.4  Addsplits [split_split, split_sum_case];
    14.5  
    14.6  (*This justifies using llist in other recursive type definitions*)
    14.7 -Goalw llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
    14.8 +Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
    14.9  by (rtac gfp_mono 1);
   14.10  by (REPEAT (ares_tac basic_monos 1));
   14.11  qed "llist_mono";
   14.12 @@ -190,7 +190,7 @@
   14.13      THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
   14.14   **)
   14.15  
   14.16 -Goalw [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
   14.17 +Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
   14.18  by (REPEAT (ares_tac basic_monos 1));
   14.19  qed "LListD_Fun_mono";
   14.20  
   14.21 @@ -335,7 +335,7 @@
   14.22  
   14.23  (*A typical use of co-induction to show membership in the gfp.
   14.24    The containing set is simply the singleton {Lconst(M)}. *)
   14.25 -Goal "!!M A. M:A ==> Lconst(M): llist(A)";
   14.26 +Goal "M:A ==> Lconst(M): llist(A)";
   14.27  by (rtac (singletonI RS llist_coinduct) 1);
   14.28  by Safe_tac;
   14.29  by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
   14.30 @@ -522,12 +522,12 @@
   14.31            Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
   14.32  
   14.33  
   14.34 -Goal "!!M. M: llist(A) ==> Lappend NIL M = M";
   14.35 +Goal "M: llist(A) ==> Lappend NIL M = M";
   14.36  by (etac LList_fun_equalityI 1);
   14.37  by (ALLGOALS Asm_simp_tac);
   14.38  qed "Lappend_NIL";
   14.39  
   14.40 -Goal "!!M. M: llist(A) ==> Lappend M NIL = M";
   14.41 +Goal "M: llist(A) ==> Lappend M NIL = M";
   14.42  by (etac LList_fun_equalityI 1);
   14.43  by (ALLGOALS Asm_simp_tac);
   14.44  qed "Lappend_NIL2";
    15.1 --- a/src/HOL/Induct/Mutil.ML	Tue Jul 14 13:33:12 1998 +0200
    15.2 +++ b/src/HOL/Induct/Mutil.ML	Wed Jul 15 10:15:13 1998 +0200
    15.3 @@ -10,7 +10,7 @@
    15.4  
    15.5  (** The union of two disjoint tilings is a tiling **)
    15.6  
    15.7 -Goal "!!t. t: tiling A ==> \
    15.8 +Goal "t: tiling A ==> \
    15.9  \              u: tiling A --> t <= Compl u --> t Un u : tiling A";
   15.10  by (etac tiling.induct 1);
   15.11  by (Simp_tac 1);
   15.12 @@ -101,7 +101,7 @@
   15.13  
   15.14  (*** Dominoes ***)
   15.15  
   15.16 -Goal "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
   15.17 +Goal "[| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
   15.18  by (eresolve_tac [domino.elim] 1);
   15.19  by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
   15.20  by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
   15.21 @@ -111,20 +111,20 @@
   15.22             THEN Blast_tac 1));
   15.23  qed "domino_singleton";
   15.24  
   15.25 -Goal "!!d. d:domino ==> finite d";
   15.26 +Goal "d:domino ==> finite d";
   15.27  by (blast_tac (claset() addSEs [domino.elim]) 1);
   15.28  qed "domino_finite";
   15.29  
   15.30  
   15.31  (*** Tilings of dominoes ***)
   15.32  
   15.33 -Goal "!!t. t:tiling domino ==> finite t";
   15.34 +Goal "t:tiling domino ==> finite t";
   15.35  by (eresolve_tac [tiling.induct] 1);
   15.36  by (rtac Finites.emptyI 1);
   15.37  by (blast_tac (claset() addSIs [finite_UnI] addIs [domino_finite]) 1);
   15.38  qed "tiling_domino_finite";
   15.39  
   15.40 -Goal "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
   15.41 +Goal "t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
   15.42  by (eresolve_tac [tiling.induct] 1);
   15.43  by (simp_tac (simpset() addsimps [evnodd_def]) 1);
   15.44  by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
   15.45 @@ -132,7 +132,7 @@
   15.46  by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
   15.47  by (Simp_tac 2 THEN assume_tac 1);
   15.48  by (Clarify_tac 1);
   15.49 -by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
   15.50 +by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd t b" 1);
   15.51  by (asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1);
   15.52  by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] 
   15.53                          addEs  [equalityE]) 1);
   15.54 @@ -140,7 +140,7 @@
   15.55  
   15.56  (*Final argument is surprisingly complex.  Note the use of small simpsets
   15.57    to avoid moving Sucs, etc.*)
   15.58 -Goal "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
   15.59 +Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
   15.60  \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
   15.61  \                |] ==> t' ~: tiling domino";
   15.62  by (rtac notI 1);
    16.1 --- a/src/HOL/Induct/Perm.ML	Tue Jul 14 13:33:12 1998 +0200
    16.2 +++ b/src/HOL/Induct/Perm.ML	Wed Jul 15 10:15:13 1998 +0200
    16.3 @@ -22,23 +22,23 @@
    16.4  (** Some examples of rule induction on permutations **)
    16.5  
    16.6  (*The form of the premise lets the induction bind xs and ys.*)
    16.7 -Goal "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
    16.8 +Goal "xs <~~> ys ==> xs=[] --> ys=[]";
    16.9  by (etac perm.induct 1);
   16.10  by (ALLGOALS Asm_simp_tac);
   16.11  qed "perm_Nil_lemma";
   16.12  
   16.13  (*A more general version is actually easier to understand!*)
   16.14 -Goal "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
   16.15 +Goal "xs <~~> ys ==> length(xs) = length(ys)";
   16.16  by (etac perm.induct 1);
   16.17  by (ALLGOALS Asm_simp_tac);
   16.18  qed "perm_length";
   16.19  
   16.20 -Goal "!!xs. xs <~~> ys ==> ys <~~> xs";
   16.21 +Goal "xs <~~> ys ==> ys <~~> xs";
   16.22  by (etac perm.induct 1);
   16.23  by (REPEAT (ares_tac perm.intrs 1));
   16.24  qed "perm_sym";
   16.25  
   16.26 -Goal "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
   16.27 +Goal "[| xs <~~> ys |] ==> x mem xs --> x mem ys";
   16.28  by (etac perm.induct 1);
   16.29  by (Fast_tac 4);
   16.30  by (ALLGOALS Asm_simp_tac);
   16.31 @@ -84,13 +84,13 @@
   16.32  by (etac perm.Cons 1);
   16.33  qed "perm_rev";
   16.34  
   16.35 -Goal "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
   16.36 +Goal "xs <~~> ys ==> l@xs <~~> l@ys";
   16.37  by (list.induct_tac "l" 1);
   16.38  by (Simp_tac 1);
   16.39  by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1);
   16.40  qed "perm_append1";
   16.41  
   16.42 -Goal "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
   16.43 +Goal "xs <~~> ys ==> xs@l <~~> ys@l";
   16.44  by (rtac (perm_append_swap RS perm.trans) 1);
   16.45  by (etac (perm_append1 RS perm.trans) 1);
   16.46  by (rtac perm_append_swap 1);
    17.1 --- a/src/HOL/Induct/PropLog.ML	Tue Jul 14 13:33:12 1998 +0200
    17.2 +++ b/src/HOL/Induct/PropLog.ML	Wed Jul 15 10:15:13 1998 +0200
    17.3 @@ -11,7 +11,7 @@
    17.4  open PropLog;
    17.5  
    17.6  (** Monotonicity **)
    17.7 -Goalw thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
    17.8 +Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
    17.9  by (rtac lfp_mono 1);
   17.10  by (REPEAT (ares_tac basic_monos 1));
   17.11  qed "thms_mono";
   17.12 @@ -34,12 +34,12 @@
   17.13  val weaken_left_Un1  =    Un_upper1 RS weaken_left;
   17.14  val weaken_left_Un2  =    Un_upper2 RS weaken_left;
   17.15  
   17.16 -Goal "!!H. H |- q ==> H |- p->q";
   17.17 +Goal "H |- q ==> H |- p->q";
   17.18  by (fast_tac (claset() addIs [thms.K,thms.MP]) 1);
   17.19  qed "weaken_right";
   17.20  
   17.21  (*The deduction theorem*)
   17.22 -Goal "!!H. insert p H |- q  ==>  H |- p->q";
   17.23 +Goal "insert p H |- q  ==>  H |- p->q";
   17.24  by (etac thms.induct 1);
   17.25  by (ALLGOALS 
   17.26      (fast_tac (claset() addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
   17.27 @@ -75,7 +75,7 @@
   17.28  Addsimps [eval_false, eval_var, eval_imp];
   17.29  
   17.30  (*Soundness of the rules wrt truth-table semantics*)
   17.31 -Goalw [sat_def] "!!H. H |- p ==> H |= p";
   17.32 +Goalw [sat_def] "H |- p ==> H |= p";
   17.33  by (etac thms.induct 1);
   17.34  by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5);
   17.35  by (ALLGOALS Asm_simp_tac);
   17.36 @@ -83,7 +83,7 @@
   17.37  
   17.38  (*** Towards the completeness proof ***)
   17.39  
   17.40 -Goal "!!H. H |- p->false ==> H |- p->q";
   17.41 +Goal "H |- p->false ==> H |- p->q";
   17.42  by (rtac deduction 1);
   17.43  by (etac (weaken_left_insert RS thms_notE) 1);
   17.44  by (rtac thms.H 1);
   17.45 @@ -206,12 +206,12 @@
   17.46  qed "completeness_0";
   17.47  
   17.48  (*A semantic analogue of the Deduction Theorem*)
   17.49 -Goalw [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
   17.50 +Goalw [sat_def] "insert p H |= q ==> H |= p->q";
   17.51  by (Simp_tac 1);
   17.52  by (Fast_tac 1);
   17.53  qed "sat_imp";
   17.54  
   17.55 -Goal "!!H. finite H ==> !p. H |= p --> H |- p";
   17.56 +Goal "finite H ==> !p. H |= p --> H |- p";
   17.57  by (etac finite_induct 1);
   17.58  by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0]));
   17.59  by (rtac (weaken_left_insert RS thms.MP) 1);
   17.60 @@ -221,6 +221,6 @@
   17.61  
   17.62  val completeness = completeness_lemma RS spec RS mp;
   17.63  
   17.64 -Goal "!!H. finite H ==> (H |- p) = (H |= p)";
   17.65 +Goal "finite H ==> (H |- p) = (H |= p)";
   17.66  by (fast_tac (claset() addSEs [soundness, completeness]) 1);
   17.67  qed "syntax_iff_semantics";
    18.1 --- a/src/HOL/Induct/SList.ML	Tue Jul 14 13:33:12 1998 +0200
    18.2 +++ b/src/HOL/Induct/SList.ML	Wed Jul 15 10:15:13 1998 +0200
    18.3 @@ -18,7 +18,7 @@
    18.4  qed "list_unfold";
    18.5  
    18.6  (*This justifies using list in other recursive type definitions*)
    18.7 -Goalw list.defs "!!A B. A<=B ==> list(A) <= list(B)";
    18.8 +Goalw list.defs "A<=B ==> list(A) <= list(B)";
    18.9  by (rtac lfp_mono 1);
   18.10  by (REPEAT (ares_tac basic_monos 1));
   18.11  qed "list_mono";
   18.12 @@ -113,7 +113,7 @@
   18.13  
   18.14  AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
   18.15  
   18.16 -Goal "!!N. N: list(A) ==> !M. N ~= CONS M N";
   18.17 +Goal "N: list(A) ==> !M. N ~= CONS M N";
   18.18  by (etac list.induct 1);
   18.19  by (ALLGOALS Asm_simp_tac);
   18.20  qed "not_CONS_self";
   18.21 @@ -191,7 +191,7 @@
   18.22  by (Simp_tac 1);
   18.23  qed "List_rec_NIL";
   18.24  
   18.25 -Goal "!!M. [| M: sexp;  N: sexp |] ==> \
   18.26 +Goal "[| M: sexp;  N: sexp |] ==> \
   18.27  \    List_rec (CONS M N) c h = h M N (List_rec N c h)";
   18.28  by (rtac (List_rec_unfold RS trans) 1);
   18.29  by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
   18.30 @@ -246,9 +246,9 @@
   18.31  by (rtac list_rec_Cons 1);
   18.32  qed "Rep_map_Cons";
   18.33  
   18.34 -Goalw [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
   18.35 +val prems = Goalw [Rep_map_def] "(!!x. f(x): A) ==> Rep_map f xs: list(A)";
   18.36  by (rtac list_induct2 1);
   18.37 -by (ALLGOALS Asm_simp_tac);
   18.38 +by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   18.39  qed "Rep_map_type";
   18.40  
   18.41  Goalw [Abs_map_def] "Abs_map g NIL = Nil";
   18.42 @@ -366,11 +366,12 @@
   18.43  by (ALLGOALS Asm_simp_tac);
   18.44  qed "map_compose2";
   18.45  
   18.46 -Goal "!!f. (!!x. f(x): sexp) ==> \
   18.47 +val prems = 
   18.48 +Goal "(!!x. f(x): sexp) ==> \
   18.49  \       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
   18.50  by (list_ind_tac "xs" 1);
   18.51  by (ALLGOALS (asm_simp_tac(simpset() addsimps
   18.52 -			   [Rep_map_type, list_sexp RS subsetD])));
   18.53 +			   (prems@[Rep_map_type, list_sexp RS subsetD]))));
   18.54  qed "Abs_Rep_map";
   18.55  
   18.56  Addsimps [append_Nil4, map_ident2];
    19.1 --- a/src/HOL/Induct/Simult.ML	Tue Jul 14 13:33:12 1998 +0200
    19.2 +++ b/src/HOL/Induct/Simult.ML	Wed Jul 15 10:15:13 1998 +0200
    19.3 @@ -23,7 +23,7 @@
    19.4  
    19.5  val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
    19.6  
    19.7 -Goalw [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
    19.8 +Goalw [TF_def] "A<=B ==> TF(A) <= TF(B)";
    19.9  by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
   19.10  qed "TF_mono";
   19.11  
    20.1 --- a/src/HOL/Induct/Term.ML	Tue Jul 14 13:33:12 1998 +0200
    20.2 +++ b/src/HOL/Induct/Term.ML	Wed Jul 15 10:15:13 1998 +0200
    20.3 @@ -17,7 +17,7 @@
    20.4  qed "term_unfold";
    20.5  
    20.6  (*This justifies using term in other recursive type definitions*)
    20.7 -Goalw term.defs "!!A B. A<=B ==> term(A) <= term(B)";
    20.8 +Goalw term.defs "A<=B ==> term(A) <= term(B)";
    20.9  by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
   20.10  qed "term_mono";
   20.11  
    21.1 --- a/src/HOL/Integ/Equiv.ML	Tue Jul 14 13:33:12 1998 +0200
    21.2 +++ b/src/HOL/Integ/Equiv.ML	Wed Jul 15 10:15:13 1998 +0200
    21.3 @@ -49,7 +49,7 @@
    21.4  by (Blast_tac 1);
    21.5  qed "equiv_class_subset";
    21.6  
    21.7 -Goal "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
    21.8 +Goal "[| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
    21.9  by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
   21.10  by (rewrite_goals_tac [equiv_def,sym_def]);
   21.11  by (Blast_tac 1);
   21.12 @@ -98,7 +98,7 @@
   21.13  
   21.14  (** Introduction/elimination rules -- needed? **)
   21.15  
   21.16 -Goalw [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
   21.17 +Goalw [quotient_def] "x:A ==> r^^{x}: A/r";
   21.18  by (Blast_tac 1);
   21.19  qed "quotientI";
   21.20  
   21.21 @@ -139,7 +139,7 @@
   21.22  **)
   21.23  
   21.24  (*Conversion rule*)
   21.25 -Goal "!!A r. [| equiv A r;  congruent r b;  a: A |] \
   21.26 +Goal "[| equiv A r;  congruent r b;  a: A |] \
   21.27  \                      ==> (UN x:r^^{a}. b(x)) = b(a)";
   21.28  by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
   21.29  by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
   21.30 @@ -244,7 +244,7 @@
   21.31  (*** Cardinality results suggested by Florian Kammueller ***)
   21.32  
   21.33  (*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
   21.34 -Goal "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
   21.35 +Goal "[| finite A; r <= A Times A |] ==> finite (A/r)";
   21.36  by (rtac finite_subset 1);
   21.37  by (etac (finite_Pow_iff RS iffD2) 2);
   21.38  by (rewtac quotient_def);
   21.39 @@ -258,7 +258,7 @@
   21.40  by (Blast_tac 1);
   21.41  qed "finite_equiv_class";
   21.42  
   21.43 -Goal "!!A. [| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] \
   21.44 +Goal "[| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] \
   21.45  \              ==> k dvd card(A)";
   21.46  by (rtac (Union_quotient RS subst) 1);
   21.47  by (assume_tac 1);
    22.1 --- a/src/HOL/Integ/Integ.ML	Tue Jul 14 13:33:12 1998 +0200
    22.2 +++ b/src/HOL/Integ/Integ.ML	Wed Jul 15 10:15:13 1998 +0200
    22.3 @@ -568,7 +568,7 @@
    22.4  by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
    22.5  qed "zless_zadd_Suc";
    22.6  
    22.7 -Goal "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
    22.8 +Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
    22.9  by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
   22.10  by (simp_tac 
   22.11      (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
   22.12 @@ -598,7 +598,7 @@
   22.13  (* z<z ==> R *)
   22.14  bind_thm ("zless_irrefl", (zless_not_refl RS notE));
   22.15  
   22.16 -Goal "!!w. z<w ==> w ~= (z::int)";
   22.17 +Goal "z<w ==> w ~= (z::int)";
   22.18  by (fast_tac (claset() addEs [zless_irrefl]) 1);
   22.19  qed "zless_not_refl2";
   22.20  
   22.21 @@ -629,30 +629,30 @@
   22.22  by (simp_tac (simpset() addsimps [zless_eq_less]) 1);
   22.23  qed "zle_eq_le";
   22.24  
   22.25 -Goalw [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
   22.26 +Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
   22.27  by (assume_tac 1);
   22.28  qed "zleI";
   22.29  
   22.30 -Goalw [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
   22.31 +Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
   22.32  by (assume_tac 1);
   22.33  qed "zleD";
   22.34  
   22.35  val zleE = make_elim zleD;
   22.36  
   22.37 -Goalw [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
   22.38 +Goalw [zle_def] "~ z <= w ==> w<(z::int)";
   22.39  by (Fast_tac 1);
   22.40  qed "not_zleE";
   22.41  
   22.42 -Goalw [zle_def] "!!z. z < w ==> z <= (w::int)";
   22.43 +Goalw [zle_def] "z < w ==> z <= (w::int)";
   22.44  by (fast_tac (claset() addEs [zless_asym]) 1);
   22.45  qed "zless_imp_zle";
   22.46  
   22.47 -Goalw [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
   22.48 +Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
   22.49  by (cut_facts_tac [zless_linear] 1);
   22.50  by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
   22.51  qed "zle_imp_zless_or_eq";
   22.52  
   22.53 -Goalw [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
   22.54 +Goalw [zle_def] "z<w | z=w ==> z <=(w::int)";
   22.55  by (cut_facts_tac [zless_linear] 1);
   22.56  by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
   22.57  qed "zless_or_eq_imp_zle";
   22.58 @@ -670,12 +670,12 @@
   22.59  by (fast_tac (claset() addIs [zless_trans]) 1);
   22.60  qed "zle_zless_trans";
   22.61  
   22.62 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
   22.63 +Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
   22.64  by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   22.65              rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
   22.66  qed "zle_trans";
   22.67  
   22.68 -Goal "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
   22.69 +Goal "[| z <= w; w <= z |] ==> z = (w::int)";
   22.70  by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   22.71              fast_tac (claset() addEs [zless_irrefl,zless_asym])]);
   22.72  qed "zle_anti_sym";
   22.73 @@ -736,7 +736,7 @@
   22.74  Addsimps [zless_eq_less, zle_eq_le,
   22.75  	  znegative_zminus_znat, not_znegative_znat]; 
   22.76  
   22.77 -Goal "!! x. (x::int) = y ==> x <= y"; 
   22.78 +Goal "(x::int) = y ==> x <= y"; 
   22.79    by (etac subst 1); by (rtac zle_refl 1); 
   22.80  qed "zequalD1"; 
   22.81  
   22.82 @@ -822,16 +822,16 @@
   22.83  Addsimps [zminus_zless_zminus, zminus_zle_zminus, 
   22.84  	  negative_eq_positive, not_znat_zless_negative]; 
   22.85  
   22.86 -Goalw [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
   22.87 +Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
   22.88    by Auto_tac; 
   22.89  qed "znegative_less_0"; 
   22.90  
   22.91 -Goalw [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
   22.92 +Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)";
   22.93    by (stac znegative_less_0 1); 
   22.94    by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); 
   22.95  qed "not_znegative_ge_0"; 
   22.96  
   22.97 -Goal "!! x. znegative x ==> ? n. x = $~ $# Suc n"; 
   22.98 +Goal "znegative x ==> ? n. x = $~ $# Suc n"; 
   22.99    by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); 
  22.100    by (etac exE 1); 
  22.101    by (rtac exI 1);
  22.102 @@ -839,7 +839,7 @@
  22.103    by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); 
  22.104  qed "znegativeD"; 
  22.105  
  22.106 -Goal "!! x. ~znegative x ==> ? n. x = $# n"; 
  22.107 +Goal "~znegative x ==> ? n. x = $# n"; 
  22.108    by (dtac (not_znegative_ge_0 RS iffD1) 1); 
  22.109    by (dtac zle_imp_zless_or_eq 1); 
  22.110    by (etac disjE 1); 
    23.1 --- a/src/HOL/Map.ML	Tue Jul 14 13:33:12 1998 +0200
    23.2 +++ b/src/HOL/Map.ML	Wed Jul 15 10:15:13 1998 +0200
    23.3 @@ -108,7 +108,7 @@
    23.4  qed "ran_empty";
    23.5  Addsimps [ran_empty];
    23.6  
    23.7 -Goalw [ran_def] "!!X. m a = None ==> ran(m[a|->b]) = insert b (ran m)";
    23.8 +Goalw [ran_def] "m a = None ==> ran(m[a|->b]) = insert b (ran m)";
    23.9  by Auto_tac;
   23.10  by (subgoal_tac "~(aa = a)" 1);
   23.11  by Auto_tac;
    24.1 --- a/src/HOL/NatDef.ML	Tue Jul 14 13:33:12 1998 +0200
    24.2 +++ b/src/HOL/NatDef.ML	Wed Jul 15 10:15:13 1998 +0200
    24.3 @@ -130,7 +130,7 @@
    24.4  
    24.5  bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
    24.6  
    24.7 -Goal "!!n. n ~= 0 ==> EX m. n = Suc m";
    24.8 +Goal "n ~= 0 ==> EX m. n = Suc m";
    24.9  by (rtac natE 1);
   24.10  by (REPEAT (Blast_tac 1));
   24.11  qed "not0_implies_Suc";
   24.12 @@ -246,7 +246,7 @@
   24.13  (* n<n ==> R *)
   24.14  bind_thm ("less_irrefl", (less_not_refl RS notE));
   24.15  
   24.16 -Goal "!!m. n<m ==> m ~= (n::nat)";
   24.17 +Goal "n<m ==> m ~= (n::nat)";
   24.18  by (blast_tac (claset() addSEs [less_irrefl]) 1);
   24.19  qed "less_not_refl2";
   24.20  
   24.21 @@ -313,14 +313,14 @@
   24.22  qed "not_gr0";
   24.23  Addsimps [not_gr0];
   24.24  
   24.25 -Goal "!!m. m<n ==> 0 < n";
   24.26 +Goal "m<n ==> 0 < n";
   24.27  by (dtac gr_implies_not0 1);
   24.28  by (Asm_full_simp_tac 1);
   24.29  qed "gr_implies_gr0";
   24.30  Addsimps [gr_implies_gr0];
   24.31  
   24.32  
   24.33 -Goal "!!m n. m<n ==> Suc(m) < Suc(n)";
   24.34 +Goal "m<n ==> Suc(m) < Suc(n)";
   24.35  by (etac rev_mp 1);
   24.36  by (nat_ind_tac "n" 1);
   24.37  by (ALLGOALS (fast_tac (claset() addEs  [less_trans, lessE])));
   24.38 @@ -354,7 +354,7 @@
   24.39  
   24.40  (** Inductive (?) properties **)
   24.41  
   24.42 -Goal "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
   24.43 +Goal "[| m<n; Suc m ~= n |] ==> Suc(m) < n";
   24.44  by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
   24.45  by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
   24.46  qed "Suc_lessI";
   24.47 @@ -375,7 +375,7 @@
   24.48  by (assume_tac 1);
   24.49  qed "Suc_lessE";
   24.50  
   24.51 -Goal "!!m n. Suc(m) < Suc(n) ==> m<n";
   24.52 +Goal "Suc(m) < Suc(n) ==> m<n";
   24.53  by (blast_tac (claset() addEs [lessE, make_elim Suc_lessD]) 1);
   24.54  qed "Suc_less_SucD";
   24.55  
   24.56 @@ -390,7 +390,7 @@
   24.57  qed "not_Suc_n_less_n";
   24.58  Addsimps [not_Suc_n_less_n];
   24.59  
   24.60 -Goal "!!i. i<j ==> j<k --> Suc i < k";
   24.61 +Goal "i<j ==> j<k --> Suc i < k";
   24.62  by (nat_ind_tac "k" 1);
   24.63  by (ALLGOALS (asm_simp_tac (simpset())));
   24.64  by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   24.65 @@ -456,7 +456,7 @@
   24.66            n_not_Suc_n, Suc_n_not_n,
   24.67            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   24.68  
   24.69 -Goal "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)";
   24.70 +Goal "(m <= Suc(n)) = (m<=n | m = Suc n)";
   24.71  by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
   24.72  by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
   24.73  qed "le_Suc_eq";
   24.74 @@ -501,7 +501,7 @@
   24.75  by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
   24.76  qed "not_less_iff_le";
   24.77  
   24.78 -Goalw [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   24.79 +Goalw [le_def] "~ m <= n ==> n<(m::nat)";
   24.80  by (Blast_tac 1);
   24.81  qed "not_leE";
   24.82  
   24.83 @@ -509,12 +509,12 @@
   24.84  by (Simp_tac 1);
   24.85  qed "not_le_iff_less";
   24.86  
   24.87 -Goalw [le_def] "!!m. m < n ==> Suc(m) <= n";
   24.88 +Goalw [le_def] "m < n ==> Suc(m) <= n";
   24.89  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   24.90  by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1);
   24.91  qed "Suc_leI";  (*formerly called lessD*)
   24.92  
   24.93 -Goalw [le_def] "!!m. Suc(m) <= n ==> m <= n";
   24.94 +Goalw [le_def] "Suc(m) <= n ==> m <= n";
   24.95  by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   24.96  qed "Suc_leD";
   24.97  
   24.98 @@ -530,25 +530,25 @@
   24.99  by (blast_tac (claset() addIs [Suc_leI, Suc_le_lessD]) 1);
  24.100  qed "Suc_le_eq";
  24.101  
  24.102 -Goalw [le_def] "!!m. m <= n ==> m <= Suc n";
  24.103 +Goalw [le_def] "m <= n ==> m <= Suc n";
  24.104  by (blast_tac (claset() addDs [Suc_lessD]) 1);
  24.105  qed "le_SucI";
  24.106  Addsimps[le_SucI];
  24.107  
  24.108  bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
  24.109  
  24.110 -Goalw [le_def] "!!m. m < n ==> m <= (n::nat)";
  24.111 +Goalw [le_def] "m < n ==> m <= (n::nat)";
  24.112  by (blast_tac (claset() addEs [less_asym]) 1);
  24.113  qed "less_imp_le";
  24.114  
  24.115  (** Equivalence of m<=n and  m<n | m=n **)
  24.116  
  24.117 -Goalw [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
  24.118 +Goalw [le_def] "m <= n ==> m < n | m=(n::nat)";
  24.119  by (cut_facts_tac [less_linear] 1);
  24.120  by (blast_tac (claset() addEs [less_irrefl,less_asym]) 1);
  24.121  qed "le_imp_less_or_eq";
  24.122  
  24.123 -Goalw [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
  24.124 +Goalw [le_def] "m<n | m=n ==> m <=(n::nat)";
  24.125  by (cut_facts_tac [less_linear] 1);
  24.126  by (blast_tac (claset() addSEs [less_irrefl] addEs [less_asym]) 1);
  24.127  qed "less_or_eq_imp_le";
  24.128 @@ -564,22 +564,22 @@
  24.129  by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
  24.130  qed "le_refl";
  24.131  
  24.132 -Goal "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
  24.133 +Goal "[| i <= j; j < k |] ==> i < (k::nat)";
  24.134  by (blast_tac (claset() addSDs [le_imp_less_or_eq]
  24.135  	                addIs [less_trans]) 1);
  24.136  qed "le_less_trans";
  24.137  
  24.138 -Goal "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
  24.139 +Goal "[| i < j; j <= k |] ==> i < (k::nat)";
  24.140  by (blast_tac (claset() addSDs [le_imp_less_or_eq]
  24.141  	                addIs [less_trans]) 1);
  24.142  qed "less_le_trans";
  24.143  
  24.144 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
  24.145 +Goal "[| i <= j; j <= k |] ==> i <= (k::nat)";
  24.146  by (blast_tac (claset() addSDs [le_imp_less_or_eq]
  24.147  	                addIs [less_or_eq_imp_le, less_trans]) 1);
  24.148  qed "le_trans";
  24.149  
  24.150 -Goal "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
  24.151 +Goal "[| m <= n; n <= m |] ==> m = (n::nat)";
  24.152  (*order_less_irrefl could make this proof fail*)
  24.153  by (blast_tac (claset() addSDs [le_imp_less_or_eq]
  24.154  	                addSEs [less_irrefl] addEs [less_asym]) 1);
    25.1 --- a/src/HOL/Ord.ML	Tue Jul 14 13:33:12 1998 +0200
    25.2 +++ b/src/HOL/Ord.ML	Wed Jul 15 10:15:13 1998 +0200
    25.3 @@ -42,8 +42,8 @@
    25.4  
    25.5  (** min **)
    25.6  
    25.7 -Goalw [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
    25.8 -by (Asm_simp_tac 1);
    25.9 +val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
   25.10 +by (simp_tac (simpset() addsimps prems) 1);
   25.11  qed "min_leastL";
   25.12  
   25.13  val prems = goalw thy [min_def]
    26.1 --- a/src/HOL/Power.ML	Tue Jul 14 13:33:12 1998 +0200
    26.2 +++ b/src/HOL/Power.ML	Wed Jul 15 10:15:13 1998 +0200
    26.3 @@ -22,7 +22,7 @@
    26.4  by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
    26.5  qed "power_mult";
    26.6  
    26.7 -Goal "!! i. 0 < i ==> 0 < i^n";
    26.8 +Goal "0 < i ==> 0 < i^n";
    26.9  by (induct_tac "n" 1);
   26.10  by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
   26.11  qed "zero_less_power";
   26.12 @@ -33,14 +33,14 @@
   26.13  by (Blast_tac 1);
   26.14  qed "le_imp_power_dvd";
   26.15  
   26.16 -Goal "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
   26.17 +Goal "[| 0 < i; i^m < i^n |] ==> m<n";
   26.18  by (rtac ccontr 1);
   26.19  by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
   26.20  by (etac zero_less_power 1);
   26.21  by (contr_tac 1);
   26.22  qed "power_less_imp_less";
   26.23  
   26.24 -Goal "!!n. k^j dvd n --> i<j --> k^i dvd n";
   26.25 +Goal "k^j dvd n --> i<j --> k^i dvd n";
   26.26  by (induct_tac "j" 1);
   26.27  by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
   26.28  by (stac mult_commute 1);
    27.1 --- a/src/HOL/Prod.ML	Tue Jul 14 13:33:12 1998 +0200
    27.2 +++ b/src/HOL/Prod.ML	Wed Jul 15 10:15:13 1998 +0200
    27.3 @@ -189,7 +189,7 @@
    27.4  by (Asm_simp_tac 1);
    27.5  qed "splitI2";
    27.6  
    27.7 -Goal "!!a b c. c a b ==> split c (a,b)";
    27.8 +Goal "c a b ==> split c (a,b)";
    27.9  by (Asm_simp_tac 1);
   27.10  qed "splitI";
   27.11  
   27.12 @@ -204,11 +204,11 @@
   27.13  	rtac (split_beta RS subst) 1,
   27.14  	rtac (hd prems) 1]);
   27.15  
   27.16 -Goal "!!R a b. split R (a,b) ==> R a b";
   27.17 +Goal "split R (a,b) ==> R a b";
   27.18  by (etac (split RS iffD1) 1);
   27.19  qed "splitD";
   27.20  
   27.21 -Goal "!!a b c. z: c a b ==> z: split c (a,b)";
   27.22 +Goal "z: c a b ==> z: split c (a,b)";
   27.23  by (Asm_simp_tac 1);
   27.24  qed "mem_splitI";
   27.25  
   27.26 @@ -241,7 +241,7 @@
   27.27  but cannot be used as rewrite rule:
   27.28  ### Cannot add premise as rewrite rule because it contains (type) unknowns:
   27.29  ### ?y = .x
   27.30 -Goal "!!P. [| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   27.31 +Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   27.32  by (rtac select_equality 1);
   27.33  by ( Simp_tac 1);
   27.34  by (split_all_tac 1);
    28.1 --- a/src/HOL/Real/Lubs.ML	Tue Jul 14 13:33:12 1998 +0200
    28.2 +++ b/src/HOL/Real/Lubs.ML	Wed Jul 15 10:15:13 1998 +0200
    28.3 @@ -10,34 +10,34 @@
    28.4  (*------------------------------------------------------------------------
    28.5                          Rules for *<= and <=*
    28.6   ------------------------------------------------------------------------*)
    28.7 -Goalw [setle_def] "!!x. ALL y: S. y <= x ==> S *<= x";
    28.8 +Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x";
    28.9  by (assume_tac 1);
   28.10  qed "setleI";
   28.11  
   28.12 -Goalw [setle_def] "!!x. [| S *<= x; y: S |] ==> y <= x";
   28.13 +Goalw [setle_def] "[| S *<= x; y: S |] ==> y <= x";
   28.14  by (Fast_tac 1);
   28.15  qed "setleD";
   28.16  
   28.17 -Goalw [setge_def] "!!x. ALL y: S. x<= y ==> x <=* S";
   28.18 +Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S";
   28.19  by (assume_tac 1);
   28.20  qed "setgeI";
   28.21  
   28.22 -Goalw [setge_def] "!!x. [| x <=* S; y: S |] ==> x <= y";
   28.23 +Goalw [setge_def] "[| x <=* S; y: S |] ==> x <= y";
   28.24  by (Fast_tac 1);
   28.25  qed "setgeD";
   28.26  
   28.27  (*------------------------------------------------------------------------
   28.28                          Rules about leastP, ub and lub
   28.29   ------------------------------------------------------------------------*)
   28.30 -Goalw [leastP_def] "!!x. leastP P x ==> P x";
   28.31 +Goalw [leastP_def] "leastP P x ==> P x";
   28.32  by (Step_tac 1);
   28.33  qed "leastPD1";
   28.34  
   28.35 -Goalw [leastP_def] "!!x. leastP P x ==> x <=* Collect P";
   28.36 +Goalw [leastP_def] "leastP P x ==> x <=* Collect P";
   28.37  by (Step_tac 1);
   28.38  qed "leastPD2";
   28.39  
   28.40 -Goal "!!x. [| leastP P x; y: Collect P |] ==> x <= y";
   28.41 +Goal "[| leastP P x; y: Collect P |] ==> x <= y";
   28.42  by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1);
   28.43  qed "leastPD3";
   28.44  
   28.45 @@ -51,19 +51,19 @@
   28.46  by (Step_tac 1);
   28.47  qed "isLubD1a";
   28.48  
   28.49 -Goalw [isUb_def] "!!x. isLub R S x ==> isUb R S x";
   28.50 +Goalw [isUb_def] "isLub R S x ==> isUb R S x";
   28.51  by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1);
   28.52  qed "isLub_isUb";
   28.53  
   28.54 -Goal "!!x. [| isLub R S x; y : S |] ==> y <= x";
   28.55 +Goal "[| isLub R S x; y : S |] ==> y <= x";
   28.56  by (blast_tac (claset() addSDs [isLubD1,setleD]) 1);
   28.57  qed "isLubD2";
   28.58  
   28.59 -Goalw [isLub_def] "!!x. isLub R S x ==> leastP(isUb R S) x";
   28.60 +Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x";
   28.61  by (assume_tac 1);
   28.62  qed "isLubD3";
   28.63  
   28.64 -Goalw [isLub_def] "!!x. leastP(isUb R S) x ==> isLub R S x";
   28.65 +Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x";
   28.66  by (assume_tac 1);
   28.67  qed "isLubI1";
   28.68  
   28.69 @@ -72,27 +72,27 @@
   28.70  by (Step_tac 1);
   28.71  qed "isLubI2";
   28.72  
   28.73 -Goalw [isUb_def] "!!x. [| isUb R S x; y : S |] ==> y <= x";
   28.74 +Goalw [isUb_def] "[| isUb R S x; y : S |] ==> y <= x";
   28.75  by (fast_tac (claset() addDs [setleD]) 1);
   28.76  qed "isUbD";
   28.77  
   28.78 -Goalw [isUb_def] "!!x. isUb R S x ==> S *<= x";
   28.79 +Goalw [isUb_def] "isUb R S x ==> S *<= x";
   28.80  by (Step_tac 1);
   28.81  qed "isUbD2";
   28.82  
   28.83 -Goalw [isUb_def] "!!x. isUb R S x ==> x: R";
   28.84 +Goalw [isUb_def] "isUb R S x ==> x: R";
   28.85  by (Step_tac 1);
   28.86  qed "isUbD2a";
   28.87  
   28.88 -Goalw [isUb_def] "!!x. [| S *<= x; x: R |] ==> isUb R S x";
   28.89 +Goalw [isUb_def] "[| S *<= x; x: R |] ==> isUb R S x";
   28.90  by (Step_tac 1);
   28.91  qed "isUbI";
   28.92  
   28.93 -Goalw [isLub_def] "!!x. [| isLub R S x; isUb R S y |] ==> x <= y";
   28.94 +Goalw [isLub_def] "[| isLub R S x; isUb R S y |] ==> x <= y";
   28.95  by (blast_tac (claset() addSIs [leastPD3]) 1);
   28.96  qed "isLub_le_isUb";
   28.97  
   28.98 -Goalw [ubs_def,isLub_def] "!!x. isLub R S x ==> x <=* ubs R S";
   28.99 +Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S";
  28.100  by (etac leastPD2 1);
  28.101  qed "isLub_ubs";
  28.102  
    29.1 --- a/src/HOL/Real/PNat.ML	Tue Jul 14 13:33:12 1998 +0200
    29.2 +++ b/src/HOL/Real/PNat.ML	Wed Jul 15 10:15:13 1998 +0200
    29.3 @@ -102,12 +102,12 @@
    29.4  
    29.5  Addsimps [zero_not_mem_pnat];
    29.6  
    29.7 -Goal "!!x. x : pnat ==> 0 < x";
    29.8 +Goal "x : pnat ==> 0 < x";
    29.9  by (dtac (pnat_unfold RS subst) 1);
   29.10  by Auto_tac;
   29.11  qed "mem_pnat_gt_zero";
   29.12  
   29.13 -Goal "!!x. 0 < x ==> x: pnat";
   29.14 +Goal "0 < x ==> x: pnat";
   29.15  by (stac pnat_unfold 1);
   29.16  by (dtac (gr_implies_not0 RS not0_implies_Suc) 1); 
   29.17  by (etac exE 1 THEN Asm_simp_tac 1);
   29.18 @@ -177,7 +177,7 @@
   29.19  
   29.20  bind_thm ("pSuc_n_not_n", n_not_pSuc_n RS not_sym);
   29.21  
   29.22 -Goal "!!n. n ~= 1p ==> EX m. n = pSuc m";
   29.23 +Goal "n ~= 1p ==> EX m. n = pSuc m";
   29.24  by (rtac pnatE 1);
   29.25  by (REPEAT (Blast_tac 1));
   29.26  qed "not1p_implies_pSuc";
   29.27 @@ -245,14 +245,14 @@
   29.28  by ((etac less_trans 1) THEN assume_tac 1);
   29.29  qed "pnat_less_trans";
   29.30  
   29.31 -Goalw [pnat_less_def] "!!x. x < (y::pnat) ==> ~ y < x";
   29.32 +Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
   29.33  by (etac less_not_sym 1);
   29.34  qed "pnat_less_not_sym";
   29.35  
   29.36  (* [| x < y; y < x |] ==> P *)
   29.37  bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE);
   29.38  
   29.39 -Goalw [pnat_less_def] "!!x. ~ y < (y::pnat)";
   29.40 +Goalw [pnat_less_def] "~ y < (y::pnat)";
   29.41  by Auto_tac;
   29.42  qed "pnat_less_not_refl";
   29.43  
   29.44 @@ -304,11 +304,11 @@
   29.45  
   29.46     (*** pnat_le ***)
   29.47  
   29.48 -Goalw [pnat_le_def] "!!x. ~ (x::pnat) < y ==> y <= x";
   29.49 +Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x";
   29.50  by (assume_tac 1);
   29.51  qed "pnat_leI";
   29.52  
   29.53 -Goalw [pnat_le_def] "!!x. (x::pnat) <= y ==> ~ y < x";
   29.54 +Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
   29.55  by (assume_tac 1);
   29.56  qed "pnat_leD";
   29.57  
   29.58 @@ -318,22 +318,22 @@
   29.59  by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
   29.60  qed "pnat_not_less_iff_le";
   29.61  
   29.62 -Goalw [pnat_le_def] "!!x. ~(x::pnat) <= y ==> y < x";
   29.63 +Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x";
   29.64  by (Blast_tac 1);
   29.65  qed "pnat_not_leE";
   29.66  
   29.67 -Goalw [pnat_le_def] "!!x. (x::pnat) < y ==> x <= y";
   29.68 +Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y";
   29.69  by (blast_tac (claset() addEs [pnat_less_asym]) 1);
   29.70  qed "pnat_less_imp_le";
   29.71  
   29.72  (** Equivalence of m<=n and  m<n | m=n **)
   29.73  
   29.74 -Goalw [pnat_le_def] "!!m. m <= n ==> m < n | m=(n::pnat)";
   29.75 +Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)";
   29.76  by (cut_facts_tac [pnat_less_linear] 1);
   29.77  by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1);
   29.78  qed "pnat_le_imp_less_or_eq";
   29.79  
   29.80 -Goalw [pnat_le_def] "!!m. m<n | m=n ==> m <=(n::pnat)";
   29.81 +Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)";
   29.82  by (cut_facts_tac [pnat_less_linear] 1);
   29.83  by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1);
   29.84  qed "pnat_less_or_eq_imp_le";
   29.85 @@ -351,19 +351,19 @@
   29.86  by (blast_tac (claset() addIs [pnat_less_trans]) 1);
   29.87  qed "pnat_le_less_trans";
   29.88  
   29.89 -Goal "!!i. [| i < j; j <= k |] ==> i < (k::pnat)";
   29.90 +Goal "[| i < j; j <= k |] ==> i < (k::pnat)";
   29.91  by (dtac pnat_le_imp_less_or_eq 1);
   29.92  by (blast_tac (claset() addIs [pnat_less_trans]) 1);
   29.93  qed "pnat_less_le_trans";
   29.94  
   29.95 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::pnat)";
   29.96 +Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)";
   29.97  by (EVERY1[dtac pnat_le_imp_less_or_eq, 
   29.98             dtac pnat_le_imp_less_or_eq,
   29.99             rtac pnat_less_or_eq_imp_le, 
  29.100             blast_tac (claset() addIs [pnat_less_trans])]);
  29.101  qed "pnat_le_trans";
  29.102  
  29.103 -Goal "!!m. [| m <= n; n <= m |] ==> m = (n::pnat)";
  29.104 +Goal "[| m <= n; n <= m |] ==> m = (n::pnat)";
  29.105  by (EVERY1[dtac pnat_le_imp_less_or_eq, 
  29.106             dtac pnat_le_imp_less_or_eq,
  29.107             blast_tac (claset() addIs [pnat_less_asym])]);
  29.108 @@ -440,7 +440,7 @@
  29.109  (*"i < j ==> i < m + j"*)
  29.110  bind_thm ("pnat_trans_less_add2", pnat_le_add2 RSN (2,pnat_less_le_trans));
  29.111  
  29.112 -Goalw [pnat_less_def] "!!i. i+j < (k::pnat) ==> i<k";
  29.113 +Goalw [pnat_less_def] "i+j < (k::pnat) ==> i<k";
  29.114  by (auto_tac (claset() addEs [add_lessD1],
  29.115      simpset() addsimps [sum_Rep_pnat_sum RS sym]));
  29.116  qed "pnat_add_lessD1";
    30.1 --- a/src/HOL/Real/PRat.ML	Tue Jul 14 13:33:12 1998 +0200
    30.2 +++ b/src/HOL/Real/PRat.ML	Wed Jul 15 10:15:13 1998 +0200
    30.3 @@ -302,7 +302,7 @@
    30.4      prat_mult_1,prat_mult_1_right]) 1);
    30.5  qed "prat_qinv_left_ex1";
    30.6  
    30.7 -Goal "!!y. x * y = $# Abs_pnat 1 ==> x = qinv y";
    30.8 +Goal "x * y = $# Abs_pnat 1 ==> x = qinv y";
    30.9  by (cut_inst_tac [("q","y")] prat_mult_qinv 1);
   30.10  by (res_inst_tac [("x1","y")] (prat_qinv_left_ex1 RS ex1E) 1);
   30.11  by (Blast_tac 1);
   30.12 @@ -580,32 +580,32 @@
   30.13  by (simp_tac (simpset() addsimps [prat_self_less_add_right]) 1);
   30.14  qed "prat_self_less_add_left";
   30.15  
   30.16 -Goalw [prat_less_def] "!!y. $#1p < y ==> (x::prat) < x * y";
   30.17 +Goalw [prat_less_def] "$#1p < y ==> (x::prat) < x * y";
   30.18  by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
   30.19      prat_add_mult_distrib2]));
   30.20  qed "prat_self_less_mult_right";
   30.21  
   30.22  (*** Properties of <= ***)
   30.23  
   30.24 -Goalw [prat_le_def] "!!w. ~(w < z) ==> z <= (w::prat)";
   30.25 +Goalw [prat_le_def] "~(w < z) ==> z <= (w::prat)";
   30.26  by (assume_tac 1);
   30.27  qed "prat_leI";
   30.28  
   30.29 -Goalw [prat_le_def] "!!w. z<=w ==> ~(w<(z::prat))";
   30.30 +Goalw [prat_le_def] "z<=w ==> ~(w<(z::prat))";
   30.31  by (assume_tac 1);
   30.32  qed "prat_leD";
   30.33  
   30.34  val prat_leE = make_elim prat_leD;
   30.35  
   30.36 -Goal "!!w. (~(w < z)) = (z <= (w::prat))";
   30.37 +Goal "(~(w < z)) = (z <= (w::prat))";
   30.38  by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
   30.39  qed "prat_less_le_iff";
   30.40  
   30.41 -Goalw [prat_le_def] "!!z. ~ z <= w ==> w<(z::prat)";
   30.42 +Goalw [prat_le_def] "~ z <= w ==> w<(z::prat)";
   30.43  by (Fast_tac 1);
   30.44  qed "not_prat_leE";
   30.45  
   30.46 -Goalw [prat_le_def] "!!z. z < w ==> z <= (w::prat)";
   30.47 +Goalw [prat_le_def] "z < w ==> z <= (w::prat)";
   30.48  by (fast_tac (claset() addEs [prat_less_asym]) 1);
   30.49  qed "prat_less_imp_le";
   30.50  
   30.51 @@ -614,7 +614,7 @@
   30.52  by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
   30.53  qed "prat_le_imp_less_or_eq";
   30.54  
   30.55 -Goalw [prat_le_def] "!!z. z<w | z=w ==> z <=(w::prat)";
   30.56 +Goalw [prat_le_def] "z<w | z=w ==> z <=(w::prat)";
   30.57  by (cut_facts_tac [prat_linear] 1);
   30.58  by (fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym]) 1);
   30.59  qed "prat_less_or_eq_imp_le";
   30.60 @@ -637,17 +637,17 @@
   30.61  by (fast_tac (claset() addIs [prat_less_trans]) 1);
   30.62  qed "prat_less_le_trans";
   30.63  
   30.64 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::prat)";
   30.65 +Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
   30.66  by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
   30.67              rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
   30.68  qed "prat_le_trans";
   30.69  
   30.70 -Goal "!!z. [| z <= w; w <= z |] ==> z = (w::prat)";
   30.71 +Goal "[| z <= w; w <= z |] ==> z = (w::prat)";
   30.72  by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
   30.73              fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
   30.74  qed "prat_le_anti_sym";
   30.75  
   30.76 -Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::prat)";
   30.77 +Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
   30.78  by (rtac not_prat_leE 1);
   30.79  by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
   30.80  qed "not_less_not_eq_prat_less";
    31.1 --- a/src/HOL/Real/PReal.ML	Tue Jul 14 13:33:12 1998 +0200
    31.2 +++ b/src/HOL/Real/PReal.ML	Wed Jul 15 10:15:13 1998 +0200
    31.3 @@ -35,7 +35,7 @@
    31.4  
    31.5  Addsimps [one_set_mem_preal];
    31.6  
    31.7 -Goalw [preal_def] "!!x. x : preal ==> {} < x";
    31.8 +Goalw [preal_def] "x : preal ==> {} < x";
    31.9  by (Fast_tac 1);
   31.10  qed "preal_psubset_empty";
   31.11  
   31.12 @@ -188,7 +188,7 @@
   31.13  (* A positive fraction not in a positive real is an upper bound *)
   31.14  (* Gleason p. 122 - Remark (1)                                  *)
   31.15  
   31.16 -Goal "!!x. x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
   31.17 +Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
   31.18  by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
   31.19  by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
   31.20  qed "not_in_preal_ub";
   31.21 @@ -488,40 +488,40 @@
   31.22                simpset() addsimps [prat_add_mult_distrib2]));
   31.23  qed "lemma_prat_add_mult_mono";
   31.24  
   31.25 -Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
   31.26 +Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
   31.27  \                  Rep_preal w; yb: Rep_preal w |] ==> \
   31.28  \                  xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
   31.29  by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
   31.30  qed "lemma_add_mult_mem_Rep_preal";
   31.31  
   31.32 -Goal "!!xb. [| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
   31.33 +Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
   31.34  \                  Rep_preal w; yb: Rep_preal w |] ==> \
   31.35  \                  yb*(xb + xc): Rep_preal (w*(z1 + z2))";
   31.36  by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);
   31.37  qed "lemma_add_mult_mem_Rep_preal1";
   31.38  
   31.39 -Goal "!!x. x: Rep_preal (w * z1 + w * z2) ==> \
   31.40 +Goal "x: Rep_preal (w * z1 + w * z2) ==> \
   31.41  \              x: Rep_preal (w * (z1 + z2))";
   31.42  by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD],
   31.43                simpset()));
   31.44 -by (forw_inst_tac [("ya","xb"),("yb","xc"),("xb","ya"),("xc","yb")] 
   31.45 +by (forw_inst_tac [("ya","xa"),("yb","xb"),("xb","ya"),("xc","yb")] 
   31.46                                     lemma_add_mult_mem_Rep_preal1 1);
   31.47  by Auto_tac;
   31.48 -by (res_inst_tac [("q1.0","xb"),("q2.0","xc")] prat_linear_less2 1);
   31.49 +by (res_inst_tac [("q1.0","xa"),("q2.0","xb")] prat_linear_less2 1);
   31.50  by (dres_inst_tac [("b","ya"),("c","yb")] lemma_prat_add_mult_mono 1);
   31.51  by (rtac (Rep_preal RS prealE_lemma3b) 1);
   31.52  by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib2]));
   31.53 -by (dres_inst_tac [("ya","xc"),("yb","xb"),("xc","ya"),("xb","yb")] 
   31.54 +by (dres_inst_tac [("ya","xb"),("yb","xa"),("xc","ya"),("xb","yb")] 
   31.55                                     lemma_add_mult_mem_Rep_preal1 1);
   31.56  by Auto_tac;
   31.57  by (dres_inst_tac [("b","yb"),("c","ya")] lemma_prat_add_mult_mono 1);
   31.58  by (rtac (Rep_preal RS prealE_lemma3b) 1);
   31.59 -by (thin_tac "xc * ya + xc * yb  : Rep_preal (w * (z1 + z2))" 1);
   31.60 +by (thin_tac "xb * ya + xb * yb  : Rep_preal (w * (z1 + z2))" 1);
   31.61  by (auto_tac (claset(),simpset() addsimps [prat_add_mult_distrib,
   31.62                prat_add_commute] @ preal_add_ac ));
   31.63  qed "lemma_preal_add_mult_distrib";
   31.64  
   31.65 -Goal "!!x. x: Rep_preal (w * (z1 + z2)) ==> \
   31.66 +Goal "x: Rep_preal (w * (z1 + z2)) ==> \
   31.67  \              x: Rep_preal (w * z1 + w * z2)";
   31.68  by (auto_tac (claset() addSDs [mem_Rep_preal_addD,mem_Rep_preal_multD]
   31.69                addSIs [bexI,mem_Rep_preal_addI,mem_Rep_preal_multI],
   31.70 @@ -610,7 +610,7 @@
   31.71  qed "preal_mem_inv_set";
   31.72  
   31.73  (*more lemmas for inverse *)
   31.74 -Goal "!!x. x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
   31.75 +Goal "x: Rep_preal(pinv(A)*A) ==> x: Rep_preal(@#($#Abs_pnat 1))";
   31.76  by (auto_tac (claset() addSDs [mem_Rep_preal_multD],
   31.77                simpset() addsimps [pinv_def,preal_prat_def] ));
   31.78  by (dtac (preal_mem_inv_set RS Abs_preal_inverse RS subst) 1);
   31.79 @@ -620,7 +620,7 @@
   31.80  qed "preal_mem_mult_invD";
   31.81  
   31.82  (*** Gleason's Lemma 9-3.4 p 122 ***)
   31.83 -Goal "!!p. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   31.84 +Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   31.85  \            ? xb : Rep_preal(A). xb + ($#p)*x : Rep_preal(A)";
   31.86  by (cut_facts_tac [mem_Rep_preal_Ex] 1);
   31.87  by (res_inst_tac [("n","p")] pnat_induct 1);
   31.88 @@ -637,7 +637,7 @@
   31.89      simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
   31.90  qed "lemma1b_gleason9_34";
   31.91  
   31.92 -Goal "!!A. ! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   31.93 +Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   31.94  by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
   31.95  by (etac exE 1);
   31.96  by (dtac not_in_preal_ub 1);
   31.97 @@ -673,7 +673,7 @@
   31.98  (******)
   31.99  
  31.100  (*** FIXME: long! ***)
  31.101 -Goal "!!A. $#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
  31.102 +Goal "$#1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
  31.103  by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
  31.104  by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
  31.105  by (Fast_tac 1);
  31.106 @@ -696,13 +696,13 @@
  31.107  by Auto_tac;
  31.108  qed "lemma_gleason9_36";
  31.109  
  31.110 -Goal "!!A. $#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
  31.111 +Goal "$#Abs_pnat 1 < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
  31.112  by (rtac lemma_gleason9_36 1);
  31.113  by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
  31.114  qed "lemma_gleason9_36a";
  31.115  
  31.116  (*** Part 2 of existence of inverse ***)
  31.117 -Goal "!!x. x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
  31.118 +Goal "x: Rep_preal(@#($#Abs_pnat 1)) ==> x: Rep_preal(pinv(A)*A)";
  31.119  by (auto_tac (claset() addSIs [mem_Rep_preal_multI],
  31.120                simpset() addsimps [pinv_def,preal_prat_def] ));
  31.121  by (rtac (preal_mem_inv_set RS Abs_preal_inverse RS ssubst) 1);
  31.122 @@ -786,11 +786,11 @@
  31.123  by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));
  31.124  qed "not_preal_leE";
  31.125  		       
  31.126 -Goal "!!w. ~(w < z) ==> z <= (w::preal)";
  31.127 +Goal "~(w < z) ==> z <= (w::preal)";
  31.128  by (fast_tac (claset() addIs [not_preal_leE]) 1);
  31.129  qed "preal_leI";
  31.130  
  31.131 -Goal "!!w. (~(w < z)) = (z <= (w::preal))";
  31.132 +Goal "(~(w < z)) = (z <= (w::preal))";
  31.133  by (fast_tac (claset() addSIs [preal_leI,preal_leD]) 1);
  31.134  qed "preal_less_le_iff";
  31.135  
  31.136 @@ -827,17 +827,17 @@
  31.137  by (fast_tac (claset() addIs [preal_less_trans]) 1);
  31.138  qed "preal_less_le_trans";
  31.139  
  31.140 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::preal)";
  31.141 +Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
  31.142  by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
  31.143              rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
  31.144  qed "preal_le_trans";
  31.145  
  31.146 -Goal "!!z. [| z <= w; w <= z |] ==> z = (w::preal)";
  31.147 +Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
  31.148  by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
  31.149              fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
  31.150  qed "preal_le_anti_sym";
  31.151  
  31.152 -Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::preal)";
  31.153 +Goal "[| ~ y < x; y ~= x |] ==> x < (y::preal)";
  31.154  by (rtac not_preal_leE 1);
  31.155  by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
  31.156  qed "not_less_not_eq_preal_less";
  31.157 @@ -849,7 +849,7 @@
  31.158  (**** Define the D required and show that it is a positive real ****)
  31.159  
  31.160  (* useful lemmas - proved elsewhere? *)
  31.161 -Goalw [psubset_def] "!!A. A < B ==> ? x. x ~: A & x : B";
  31.162 +Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
  31.163  by (etac conjE 1);
  31.164  by (etac swap 1);
  31.165  by (etac equalityI 1);
  31.166 @@ -911,7 +911,7 @@
  31.167  qed "preal_less_set_not_prat_set";
  31.168  
  31.169  (** Part 3 of Dedekind sections def **)
  31.170 -Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  31.171 +Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  31.172   \      !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  31.173  by Auto_tac;
  31.174  by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
  31.175 @@ -919,7 +919,7 @@
  31.176  by Auto_tac;
  31.177  qed "preal_less_set_lemma3";
  31.178  
  31.179 -Goal "!!A. A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  31.180 +Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
  31.181  \       Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
  31.182  by Auto_tac;
  31.183  by (dtac (Rep_preal RS prealE_lemma4a) 1);
  31.184 @@ -954,7 +954,7 @@
  31.185  
  31.186  (** proving that B <= A + D  --- trickier **)
  31.187  (** lemma **)
  31.188 -Goal "!!x. x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
  31.189 +Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
  31.190  by (dtac (Rep_preal RS prealE_lemma4a) 1);
  31.191  by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
  31.192  qed "lemma_sum_mem_Rep_preal_ex";
  31.193 @@ -1115,7 +1115,7 @@
  31.194  (*** Completeness of preal ***)
  31.195  
  31.196  (*** prove that supremum is a cut ***)
  31.197 -Goal "!!P. ? (X::preal). X: P ==> \
  31.198 +Goal "? (X::preal). X: P ==> \
  31.199  \         ? q.  q: {w. ? X. X : P & w : Rep_preal X}";
  31.200  by Safe_tac;
  31.201  by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
  31.202 @@ -1123,14 +1123,14 @@
  31.203  qed "preal_sup_mem_Ex";
  31.204  
  31.205  (** Part 1 of Dedekind def **)
  31.206 -Goal "!!P. ? (X::preal). X: P ==> \
  31.207 +Goal "? (X::preal). X: P ==> \
  31.208  \         {} < {w. ? X : P. w : Rep_preal X}";
  31.209  by (dtac preal_sup_mem_Ex 1);
  31.210  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
  31.211  qed "preal_sup_set_not_empty";
  31.212  
  31.213  (** Part 2 of Dedekind sections def **) 
  31.214 -Goalw [preal_less_def] "!!P. ? Y. (! X: P. X < Y)  \             
  31.215 +Goalw [preal_less_def] "? Y. (! X: P. X < Y)  \             
  31.216  \         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
  31.217  by (auto_tac (claset(),simpset() addsimps [psubset_def]));
  31.218  by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
  31.219 @@ -1139,7 +1139,7 @@
  31.220  by (auto_tac (claset() addSDs [bspec],simpset()));
  31.221  qed "preal_sup_not_mem_Ex";
  31.222  
  31.223 -Goalw [preal_le_def] "!!P. ? Y. (! X: P. X <= Y)  \
  31.224 +Goalw [preal_le_def] "? Y. (! X: P. X <= Y)  \
  31.225  \         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
  31.226  by (Step_tac 1);
  31.227  by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
  31.228 @@ -1148,7 +1148,7 @@
  31.229  by (auto_tac (claset() addSDs [bspec],simpset()));
  31.230  qed "preal_sup_not_mem_Ex1";
  31.231  
  31.232 -Goal "!!P. ? Y. (! X: P. X < Y)  \                                    
  31.233 +Goal "? Y. (! X: P. X < Y)  \                                    
  31.234  \         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";       (**)
  31.235  by (dtac preal_sup_not_mem_Ex 1);
  31.236  by (auto_tac (claset() addSIs [psubsetI],simpset()));
  31.237 @@ -1156,7 +1156,7 @@
  31.238  by Auto_tac;
  31.239  qed "preal_sup_set_not_prat_set";
  31.240  
  31.241 -Goal "!!P. ? Y. (! X: P. X <= Y)  \
  31.242 +Goal "? Y. (! X: P. X <= Y)  \
  31.243  \         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
  31.244  by (dtac preal_sup_not_mem_Ex1 1);
  31.245  by (auto_tac (claset() addSIs [psubsetI],simpset()));
  31.246 @@ -1165,31 +1165,31 @@
  31.247  qed "preal_sup_set_not_prat_set1";
  31.248  
  31.249  (** Part 3 of Dedekind sections def **)
  31.250 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
  31.251 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
  31.252  \         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
  31.253  \             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";         (**)
  31.254  by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
  31.255  qed "preal_sup_set_lemma3";
  31.256  
  31.257 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  31.258 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  31.259  \         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
  31.260  \             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
  31.261  by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
  31.262  qed "preal_sup_set_lemma3_1";
  31.263  
  31.264 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
  31.265 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
  31.266  \         ==>  !y: {w. ? X: P. w: Rep_preal X}. \                        
  31.267  \             Bex {w. ? X: P. w: Rep_preal X} (op < y)";                (**)
  31.268  by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
  31.269  qed "preal_sup_set_lemma4";
  31.270  
  31.271 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  31.272 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  31.273  \         ==>  !y: {w. ? X: P. w: Rep_preal X}. \
  31.274  \             Bex {w. ? X: P. w: Rep_preal X} (op < y)";
  31.275  by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
  31.276  qed "preal_sup_set_lemma4_1";
  31.277  
  31.278 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
  31.279 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
  31.280  \         ==> {w. ? X: P. w: Rep_preal(X)}: preal";                      (**)
  31.281  by (rtac prealI2 1);
  31.282  by (rtac preal_sup_set_not_empty 1);
  31.283 @@ -1199,7 +1199,7 @@
  31.284  by Auto_tac;
  31.285  qed "preal_sup";
  31.286  
  31.287 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  31.288 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
  31.289  \         ==> {w. ? X: P. w: Rep_preal(X)}: preal";
  31.290  by (rtac prealI2 1);
  31.291  by (rtac preal_sup_set_not_empty 1);
  31.292 @@ -1209,27 +1209,27 @@
  31.293  by Auto_tac;
  31.294  qed "preal_sup1";
  31.295  
  31.296 -Goalw [psup_def] "!!P. ? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
  31.297 +Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
  31.298  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  31.299  by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
  31.300  by Auto_tac;
  31.301  qed "preal_psup_leI";
  31.302  
  31.303 -Goalw [psup_def] "!!P. ? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
  31.304 +Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
  31.305  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  31.306  by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
  31.307  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  31.308  qed "preal_psup_leI2";
  31.309  
  31.310 -Goal "!!P. [| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
  31.311 +Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
  31.312  by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
  31.313  qed "preal_psup_leI2b";
  31.314  
  31.315 -Goal "!!P. [| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
  31.316 +Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
  31.317  by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
  31.318  qed "preal_psup_leI2a";
  31.319  
  31.320 -Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
  31.321 +Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
  31.322  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  31.323  by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
  31.324  by (rotate_tac 1 2);
  31.325 @@ -1237,7 +1237,7 @@
  31.326  by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
  31.327  qed "psup_le_ub";
  31.328  
  31.329 -Goalw [psup_def] "!!P. [| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
  31.330 +Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
  31.331  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
  31.332  by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
  31.333  by (rotate_tac 1 2);
  31.334 @@ -1247,7 +1247,7 @@
  31.335  qed "psup_le_ub1";
  31.336  
  31.337  (** supremum property **)
  31.338 -Goal "!!P. [|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
  31.339 +Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
  31.340  \         ==> (!Y. (? X: P. Y < X) = (Y < psup P))";              
  31.341  by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
  31.342  by (Fast_tac 1);
  31.343 @@ -1267,12 +1267,12 @@
  31.344      (****** Embedding ******)
  31.345  (*** mapping from prat into preal ***)
  31.346  
  31.347 -Goal "!!z1. x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
  31.348 +Goal "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1";
  31.349  by (dres_inst_tac [("x","z1 * qinv (z1 + z2)")] prat_mult_less2_mono1 1);
  31.350  by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  31.351  qed "lemma_preal_rat_less";
  31.352  
  31.353 -Goal "!!z1. x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
  31.354 +Goal "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2";
  31.355  by (stac prat_add_commute 1);
  31.356  by (dtac (prat_add_commute RS subst) 1);
  31.357  by (etac lemma_preal_rat_less 1);
  31.358 @@ -1291,13 +1291,13 @@
  31.359       prat_add_mult_distrib2 RS sym] @ prat_mult_ac) 1);
  31.360  qed "preal_prat_add";
  31.361  
  31.362 -Goal "!!xa. x < xa ==> x*z1*qinv(xa) < z1";
  31.363 +Goal "x < xa ==> x*z1*qinv(xa) < z1";
  31.364  by (dres_inst_tac [("x","z1 * qinv xa")] prat_mult_less2_mono1 1);
  31.365  by (dtac (prat_mult_left_commute RS subst) 1);
  31.366  by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
  31.367  qed "lemma_preal_rat_less3";
  31.368  
  31.369 -Goal "!!xa. xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
  31.370 +Goal "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2";
  31.371  by (dres_inst_tac [("x","z2 * qinv(z1*z2)")] prat_mult_less2_mono1 1);
  31.372  by (dtac (prat_mult_left_commute RS subst) 1);
  31.373  by (asm_full_simp_tac (simpset() addsimps prat_mult_ac) 1);
    32.1 --- a/src/HOL/Real/RComplete.ML	Tue Jul 14 13:33:12 1998 +0200
    32.2 +++ b/src/HOL/Real/RComplete.ML	Wed Jul 15 10:15:13 1998 +0200
    32.3 @@ -24,7 +24,7 @@
    32.4             Completeness theorem for the positive reals(again)
    32.5   ----------------------------------------------------------------*)
    32.6  
    32.7 -Goal "!!S. [| ALL x: S. 0r < x; \
    32.8 +Goal "[| ALL x: S. 0r < x; \
    32.9  \                 EX x. x: S; \
   32.10  \                 EX u. isUb (UNIV::real set) S u \
   32.11  \              |] ==> EX t. isLub (UNIV::real set) S t";
   32.12 @@ -85,7 +85,7 @@
   32.13  by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
   32.14  qed "lemma_le_swap2";
   32.15  
   32.16 -Goal "!!x. [| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
   32.17 +Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
   32.18  by (dtac real_add_less_mono 1);
   32.19  by (assume_tac 1);
   32.20  by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1);
   32.21 @@ -104,13 +104,13 @@
   32.22          real_add_minus_left,real_add_zero_left]) 1);
   32.23  qed "lemma_real_complete2";
   32.24  
   32.25 -Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
   32.26 +Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
   32.27  by (rtac (lemma_le_swap2 RS iffD2) 1);
   32.28  by (etac lemma_real_complete2 1);
   32.29  by (assume_tac 1);
   32.30  qed "lemma_real_complete2a";
   32.31  
   32.32 -Goal "!!x. [| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
   32.33 +Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
   32.34  by (rotate_tac 1 1);
   32.35  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   32.36  by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
   32.37 @@ -173,7 +173,7 @@
   32.38        real_add_minus,real_add_minus_left,real_add_zero_right]));
   32.39  qed "lemma_arch";
   32.40  
   32.41 -Goal "!!x. 0r < x ==> EX n. rinv(%%#n) < x";
   32.42 +Goal "0r < x ==> EX n. rinv(%%#n) < x";
   32.43  by (stac real_nat_rinv_Ex_iff 1);
   32.44  by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
   32.45  by (fold_tac [real_le_def]);
    33.1 --- a/src/HOL/Real/Real.ML	Tue Jul 14 13:33:12 1998 +0200
    33.2 +++ b/src/HOL/Real/Real.ML	Wed Jul 15 10:15:13 1998 +0200
    33.3 @@ -239,7 +239,7 @@
    33.4      real_add_zero_right,real_add_zero_left]) 1);
    33.5  qed "real_minus_left_ex1";
    33.6  
    33.7 -Goal "!!y. x + y = 0r ==> x = %~y";
    33.8 +Goal "x + y = 0r ==> x = %~y";
    33.9  by (cut_inst_tac [("z","y")] real_add_minus_left 1);
   33.10  by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
   33.11  by (Blast_tac 1);
   33.12 @@ -451,19 +451,19 @@
   33.13                simpset() addsimps [real_mult_inv_left]));
   33.14  qed "real_mult_inv_right";
   33.15  
   33.16 -Goal "!!a. (c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
   33.17 +Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
   33.18  by Auto_tac;
   33.19  by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   33.20  by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   33.21  qed "real_mult_left_cancel";
   33.22      
   33.23 -Goal "!!a. (c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
   33.24 +Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
   33.25  by (Step_tac 1);
   33.26  by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   33.27  by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   33.28  qed "real_mult_right_cancel";
   33.29  
   33.30 -Goalw [rinv_def] "!!x. x ~= 0r ==> rinv(x) ~= 0r";
   33.31 +Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
   33.32  by (forward_tac [real_mult_inv_left_ex] 1);
   33.33  by (etac exE 1);
   33.34  by (rtac selectI2 1);
   33.35 @@ -473,7 +473,7 @@
   33.36  
   33.37  Addsimps [real_mult_inv_left,real_mult_inv_right];
   33.38  
   33.39 -Goal "!!x. x ~= 0r ==> rinv(rinv x) = x";
   33.40 +Goal "x ~= 0r ==> rinv(rinv x) = x";
   33.41  by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
   33.42  by (etac rinv_not_zero 1);
   33.43  by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
   33.44 @@ -488,7 +488,7 @@
   33.45      [real_zero_not_eq_one RS not_sym]));
   33.46  qed "real_rinv_1";
   33.47  
   33.48 -Goal "!!x. x ~= 0r ==> rinv(%~x) = %~rinv(x)";
   33.49 +Goal "x ~= 0r ==> rinv(%~x) = %~rinv(x)";
   33.50  by (res_inst_tac [("c1","%~x")] (real_mult_right_cancel RS iffD1) 1);
   33.51  by Auto_tac;
   33.52  qed "real_minus_rinv";
   33.53 @@ -637,19 +637,19 @@
   33.54  qed "real_preal_trichotomy";
   33.55  
   33.56  Goal "!!x. [| !!m. x = %#m ==> P; \
   33.57 -\            x = 0r ==> P; \
   33.58 -\            !!m. x = %~(%#m) ==> P |] ==> P";
   33.59 +\             x = 0r ==> P; \
   33.60 +\             !!m. x = %~(%#m) ==> P |] ==> P";
   33.61  by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
   33.62  by Auto_tac;
   33.63  qed "real_preal_trichotomyE";
   33.64  
   33.65 -Goalw [real_preal_def] "!!m1 m2. %#m1 < %#m2 ==> m1 < m2";
   33.66 +Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
   33.67  by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
   33.68  by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
   33.69  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   33.70  qed "real_preal_lessD";
   33.71  
   33.72 -Goal "!!m1 m2. m1 < m2 ==> %#m1 < %#m2";
   33.73 +Goal "m1 < m2 ==> %#m1 < %#m2";
   33.74  by (dtac preal_less_add_left_Ex 1);
   33.75  by (auto_tac (claset(),simpset() addsimps [real_preal_add,
   33.76      real_preal_def,real_less_def]));
   33.77 @@ -743,7 +743,7 @@
   33.78                 addEs [real_less_irrefl]) 1);
   33.79  qed "real_preal_not_minus_gt_all";
   33.80  
   33.81 -Goal "!!m1 m2. %~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
   33.82 +Goal "%~ %#m1 < %~ %#m2 ==> %#m2 < %#m1";
   33.83  by (auto_tac (claset(),simpset() addsimps 
   33.84      [real_preal_def,real_less_def,real_minus]));
   33.85  by (REPEAT(rtac exI 1));
   33.86 @@ -754,7 +754,7 @@
   33.87  by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   33.88  qed "real_preal_minus_less_rev1";
   33.89  
   33.90 -Goal "!!m1 m2. %#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
   33.91 +Goal "%#m1 < %#m2 ==> %~ %#m2 < %~ %#m1";
   33.92  by (auto_tac (claset(),simpset() addsimps 
   33.93      [real_preal_def,real_less_def,real_minus]));
   33.94  by (REPEAT(rtac exI 1));
   33.95 @@ -790,25 +790,25 @@
   33.96  
   33.97  (*** Properties of <= ***)
   33.98  
   33.99 -Goalw [real_le_def] "!!w. ~(w < z) ==> z <= (w::real)";
  33.100 +Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
  33.101  by (assume_tac 1);
  33.102  qed "real_leI";
  33.103  
  33.104 -Goalw [real_le_def] "!!w. z<=w ==> ~(w<(z::real))";
  33.105 +Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
  33.106  by (assume_tac 1);
  33.107  qed "real_leD";
  33.108  
  33.109  val real_leE = make_elim real_leD;
  33.110  
  33.111 -Goal "!!w. (~(w < z)) = (z <= (w::real))";
  33.112 +Goal "(~(w < z)) = (z <= (w::real))";
  33.113  by (fast_tac (claset() addSIs [real_leI,real_leD]) 1);
  33.114  qed "real_less_le_iff";
  33.115  
  33.116 -Goalw [real_le_def] "!!z. ~ z <= w ==> w<(z::real)";
  33.117 +Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
  33.118  by (Fast_tac 1);
  33.119  qed "not_real_leE";
  33.120  
  33.121 -Goalw [real_le_def] "!!z. z < w ==> z <= (w::real)";
  33.122 +Goalw [real_le_def] "z < w ==> z <= (w::real)";
  33.123  by (fast_tac (claset() addEs [real_less_asym]) 1);
  33.124  qed "real_less_imp_le";
  33.125  
  33.126 @@ -817,7 +817,7 @@
  33.127  by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
  33.128  qed "real_le_imp_less_or_eq";
  33.129  
  33.130 -Goalw [real_le_def] "!!z. z<w | z=w ==> z <=(w::real)";
  33.131 +Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
  33.132  by (cut_facts_tac [real_linear] 1);
  33.133  by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
  33.134  qed "real_less_or_eq_imp_le";
  33.135 @@ -840,17 +840,17 @@
  33.136  by (fast_tac (claset() addIs [real_less_trans]) 1);
  33.137  qed "real_less_le_trans";
  33.138  
  33.139 -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::real)";
  33.140 +Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
  33.141  by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
  33.142              rtac real_less_or_eq_imp_le, fast_tac (claset() addIs [real_less_trans])]);
  33.143  qed "real_le_trans";
  33.144  
  33.145 -Goal "!!z. [| z <= w; w <= z |] ==> z = (w::real)";
  33.146 +Goal "[| z <= w; w <= z |] ==> z = (w::real)";
  33.147  by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
  33.148              fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
  33.149  qed "real_le_anti_sym";
  33.150  
  33.151 -Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::real)";
  33.152 +Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
  33.153  by (rtac not_real_leE 1);
  33.154  by (fast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
  33.155  qed "not_less_not_eq_real_less";
  33.156 @@ -879,23 +879,23 @@
  33.157       real_preal_not_minus_gt_zero RS notE]) 1);
  33.158  qed "real_gt_zero_preal_Ex";
  33.159  
  33.160 -Goal "!!x. %#z < x ==> ? y. x = %#y";
  33.161 +Goal "%#z < x ==> ? y. x = %#y";
  33.162  by (blast_tac (claset() addSDs [real_preal_zero_less RS real_less_trans]
  33.163                 addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
  33.164  qed "real_gt_preal_preal_Ex";
  33.165  
  33.166 -Goal "!!x. %#z <= x ==> ? y. x = %#y";
  33.167 +Goal "%#z <= x ==> ? y. x = %#y";
  33.168  by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
  33.169                real_gt_preal_preal_Ex]) 1);
  33.170  qed "real_ge_preal_preal_Ex";
  33.171  
  33.172 -Goal "!!y. y <= 0r ==> !x. y < %#x";
  33.173 +Goal "y <= 0r ==> !x. y < %#x";
  33.174  by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
  33.175                addIs [real_preal_zero_less RSN(2,real_less_trans)],
  33.176                simpset() addsimps [real_preal_zero_less]));
  33.177  qed "real_less_all_preal";
  33.178  
  33.179 -Goal "!!y. ~ 0r < y ==> !x. y < %#x";
  33.180 +Goal "~ 0r < y ==> !x. y < %#x";
  33.181  by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
  33.182  qed "real_less_all_real2";
  33.183  
  33.184 @@ -937,19 +937,19 @@
  33.185  
  33.186  (* lemmas *)
  33.187  (** change naff name(s)! **)
  33.188 -Goal "!!S. (W < S) ==> (0r < S + %~W)";
  33.189 +Goal "(W < S) ==> (0r < S + %~W)";
  33.190  by (dtac real_less_add_positive_left_Ex 1);
  33.191  by (auto_tac (claset(),simpset() addsimps [real_add_minus,
  33.192      real_add_zero_right] @ real_add_ac));
  33.193  qed "real_less_sum_gt_zero";
  33.194  
  33.195  Goal "!!S. T = S + W ==> S = T + %~W";
  33.196 -by (asm_simp_tac (simpset() addsimps [real_add_minus,
  33.197 -    real_add_zero_right] @ real_add_ac) 1);
  33.198 +by (asm_simp_tac (simpset() addsimps [real_add_minus, real_add_zero_right] 
  33.199 +		                     @ real_add_ac) 1);
  33.200  qed "real_lemma_change_eq_subj";
  33.201  
  33.202  (* FIXME: long! *)
  33.203 -Goal "!!W. (0r < S + %~W) ==> (W < S)";
  33.204 +Goal "(0r < S + %~W) ==> (W < S)";
  33.205  by (rtac ccontr 1);
  33.206  by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
  33.207  by (auto_tac (claset(),
  33.208 @@ -976,7 +976,7 @@
  33.209  by (simp_tac (simpset() addsimps [real_add_commute]) 1);
  33.210  qed "real_less_swap_iff";
  33.211  
  33.212 -Goal "!!T. [| R + L = S; 0r < L |] ==> R < S";
  33.213 +Goal "[| R + L = S; 0r < L |] ==> R < S";
  33.214  by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
  33.215  by (auto_tac (claset(),simpset() addsimps [
  33.216      real_add_minus,real_add_zero_right] @ real_add_ac));
  33.217 @@ -1075,11 +1075,11 @@
  33.218  (*** Completeness of reals ***)
  33.219  (** use supremum property of preal and theorems about real_preal **)
  33.220                (*** a few lemmas ***)
  33.221 -Goal "!!P y. ! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
  33.222 +Goal "! x:P. 0r < x ==> ((? x:P. y < x) = (? X. %#X : P & y < %#X))";
  33.223  by (blast_tac (claset() addSDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
  33.224  qed "real_sup_lemma1";
  33.225  
  33.226 -Goal "!!P. [| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
  33.227 +Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
  33.228  \         ==> (? X. X: {w. %#w : P}) & (? Y. !X: {w. %#w : P}. X < Y)";
  33.229  by (rtac conjI 1);
  33.230  by (blast_tac (claset() addDs [bspec,real_gt_zero_preal_Ex RS iffD1]) 1);
  33.231 @@ -1101,7 +1101,7 @@
  33.232  (* Supremum property for the set of positive reals *)
  33.233  (* FIXME: long proof - can be improved - need only have one case split *)
  33.234  (* will do for now *)
  33.235 -Goal "!!P. [| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
  33.236 +Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
  33.237  \         ==> (? S. !y. (? x: P. y < x) = (y < S))";
  33.238  by (res_inst_tac [("x","%#psup({w. %#w : P})")] exI 1);
  33.239  by Auto_tac;
  33.240 @@ -1156,7 +1156,7 @@
  33.241      real_add_minus_left,real_add_zero_left]) 1);
  33.242  qed "real_less_add_left_cancel";
  33.243  
  33.244 -Goal "!!x. [| 0r < x; 0r < y |] ==> 0r < x + y";
  33.245 +Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
  33.246  by (REPEAT(dtac (real_gt_zero_preal_Ex RS iffD1) 1));
  33.247  by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
  33.248  by (Step_tac 1);
  33.249 @@ -1267,7 +1267,7 @@
  33.250  by (Blast_tac 1);
  33.251  qed "real_nat_less_zero";
  33.252  
  33.253 -Goal "!!n. 1r <= %%#n";
  33.254 +Goal "1r <= %%#n";
  33.255  by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
  33.256  by (nat_ind_tac "n" 1);
  33.257  by (auto_tac (claset(),simpset () 
  33.258 @@ -1284,7 +1284,7 @@
  33.259      real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
  33.260  qed "real_nat_rinv_not_zero";
  33.261  
  33.262 -Goal "!!x. rinv(%%#x) = rinv(%%#y) ==> x = y";
  33.263 +Goal "rinv(%%#x) = rinv(%%#y) ==> x = y";
  33.264  by (rtac (inj_real_nat RS injD) 1);
  33.265  by (res_inst_tac [("n2","x")] 
  33.266      (real_nat_rinv_not_zero RS real_mult_left_cancel RS iffD1) 1);
  33.267 @@ -1294,7 +1294,7 @@
  33.268      real_not_refl2 RS not_sym)]) 1);
  33.269  qed "real_nat_rinv_inj";
  33.270  
  33.271 -Goal "!!x. 0r < x ==> 0r < rinv x";
  33.272 +Goal "0r < x ==> 0r < rinv x";
  33.273  by (EVERY1[rtac ccontr, dtac real_leI]);
  33.274  by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
  33.275  by (forward_tac [real_not_refl2 RS not_sym] 1);
  33.276 @@ -1305,7 +1305,7 @@
  33.277      simpset() addsimps [real_minus_mult_eq1 RS sym]));
  33.278  qed "real_rinv_gt_zero";
  33.279  
  33.280 -Goal "!!x. x < 0r ==> rinv x < 0r";
  33.281 +Goal "x < 0r ==> rinv x < 0r";
  33.282  by (forward_tac [real_not_refl2] 1);
  33.283  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
  33.284  by (rtac (real_minus_zero_less_iff RS iffD1) 1);
  33.285 @@ -1370,12 +1370,12 @@
  33.286  by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
  33.287  qed "real_mult_less_cancel2";
  33.288  
  33.289 -Goal "!!z. 0r < z ==> (x*z < y*z) = (x < y)";
  33.290 +Goal "0r < z ==> (x*z < y*z) = (x < y)";
  33.291  by (blast_tac (claset() addIs [real_mult_less_mono1,
  33.292      real_mult_less_cancel1]) 1);
  33.293  qed "real_mult_less_iff1";
  33.294  
  33.295 -Goal "!!z. 0r < z ==> (z*x < z*y) = (x < y)";
  33.296 +Goal "0r < z ==> (z*x < z*y) = (x < y)";
  33.297  by (blast_tac (claset() addIs [real_mult_less_mono2,
  33.298      real_mult_less_cancel2]) 1);
  33.299  qed "real_mult_less_iff2";
  33.300 @@ -1432,7 +1432,7 @@
  33.301  
  33.302  Addsimps [real_nat_less_iff];
  33.303  
  33.304 -Goal "!!u. 0r < u  ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
  33.305 +Goal "0r < u  ==> (u < rinv (%%#n)) = (%%#n < rinv(u))";
  33.306  by (Step_tac 1);
  33.307  by (res_inst_tac [("n2","n")] (real_nat_less_zero RS 
  33.308      real_rinv_gt_zero RS real_mult_less_cancel1) 1);
  33.309 @@ -1447,7 +1447,7 @@
  33.310      real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
  33.311  qed "real_nat_less_rinv_iff";
  33.312  
  33.313 -Goal "!!x. 0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
  33.314 +Goal "0r < u ==> (u = rinv(%%#n)) = (%%#n = rinv u)";
  33.315  by (auto_tac (claset(),simpset() addsimps [real_rinv_rinv,
  33.316      real_nat_less_zero,real_not_refl2 RS not_sym]));
  33.317  qed "real_nat_rinv_eq_iff";
    34.1 --- a/src/HOL/Real/RealAbs.ML	Tue Jul 14 13:33:12 1998 +0200
    34.2 +++ b/src/HOL/Real/RealAbs.ML	Wed Jul 15 10:15:13 1998 +0200
    34.3 @@ -37,7 +37,7 @@
    34.4  by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
    34.5  qed "rabs_minus_eqI2";
    34.6  
    34.7 -Goal "!!x. x<=0r ==> rabs x = %~x";
    34.8 +Goal "x<=0r ==> rabs x = %~x";
    34.9  by (dtac real_le_imp_less_or_eq 1);
   34.10  by (fast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
   34.11  qed "rabs_minus_eqI1";
   34.12 @@ -86,7 +86,7 @@
   34.13      simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
   34.14  qed "rabs_mult";
   34.15  
   34.16 -Goalw [rabs_def] "!!x. x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
   34.17 +Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
   34.18  by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] 
   34.19      setloop (split_tac [expand_if])));
   34.20  by (ALLGOALS(dtac not_real_leE));
   34.21 @@ -142,7 +142,7 @@
   34.22  by (REPEAT (ares_tac [real_add_less_mono] 1));
   34.23  qed "rabs_add_less";
   34.24  
   34.25 -Goal "!!x y. [| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
   34.26 +Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ %~y) < r+s";
   34.27  by (rotate_tac 1 1);
   34.28  by (dtac (rabs_minus_cancel RS ssubst) 1);
   34.29  by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
   34.30 @@ -175,13 +175,13 @@
   34.31  			     real_le_less_trans]) 1);
   34.32  qed "rabs_mult_less";
   34.33  
   34.34 -Goal "!!x. [| rabs x < r; rabs y < s |] \
   34.35 +Goal "[| rabs x < r; rabs y < s |] \
   34.36  \          ==> rabs(x)*rabs(y)<r*s";
   34.37  by (auto_tac (claset() addIs [rabs_mult_less],
   34.38                simpset() addsimps [rabs_mult RS sym]));
   34.39  qed "rabs_mult_less2";
   34.40  
   34.41 -Goal "!! x y r. 1r < rabs x ==> rabs y <= rabs(x*y)";
   34.42 +Goal "1r < rabs x ==> rabs y <= rabs(x*y)";
   34.43  by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1);
   34.44  by (EVERY1[etac disjE,rtac real_less_imp_le]);
   34.45  by (dres_inst_tac [("W","1r")]  real_less_sum_gt_zero 1);
   34.46 @@ -194,11 +194,11 @@
   34.47  by (asm_full_simp_tac (simpset() addsimps [real_le_refl,rabs_mult]) 1);
   34.48  qed "rabs_mult_le";
   34.49  
   34.50 -Goal "!!x. [| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
   34.51 +Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
   34.52  by (fast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1);
   34.53  qed "rabs_mult_gt";
   34.54  
   34.55 -Goal "!!r. rabs(x)<r ==> 0r<r";
   34.56 +Goal "rabs(x)<r ==> 0r<r";
   34.57  by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1);
   34.58  qed "rabs_less_gt_zero";
   34.59  
   34.60 @@ -217,7 +217,7 @@
   34.61                              rabs_zero,rabs_minus_zero]) 1);
   34.62  qed "rabs_disj";
   34.63  
   34.64 -Goal "!!x. rabs x = y ==> x = y | %~x = y";
   34.65 +Goal "rabs x = y ==> x = y | %~x = y";
   34.66  by (dtac sym 1);
   34.67  by (hyp_subst_tac 1);
   34.68  by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
    35.1 --- a/src/HOL/RelPow.ML	Tue Jul 14 13:33:12 1998 +0200
    35.2 +++ b/src/HOL/RelPow.ML	Wed Jul 15 10:15:13 1998 +0200
    35.3 @@ -15,7 +15,7 @@
    35.4  by (Simp_tac 1);
    35.5  qed "rel_pow_0_I";
    35.6  
    35.7 -Goal "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    35.8 +Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    35.9  by (Simp_tac  1);
   35.10  by (Blast_tac 1);
   35.11  qed "rel_pow_Suc_I";
    36.1 --- a/src/HOL/Relation.ML	Tue Jul 14 13:33:12 1998 +0200
    36.2 +++ b/src/HOL/Relation.ML	Wed Jul 15 10:15:13 1998 +0200
    36.3 @@ -68,7 +68,7 @@
    36.4  by (Blast_tac 1);
    36.5  qed "O_assoc";
    36.6  
    36.7 -Goal "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    36.8 +Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    36.9  by (Blast_tac 1);
   36.10  qed "comp_mono";
   36.11  
   36.12 @@ -91,17 +91,17 @@
   36.13  
   36.14  (** Natural deduction for r^-1 **)
   36.15  
   36.16 -Goalw [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
   36.17 +Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
   36.18  by (Simp_tac 1);
   36.19  qed "converse_iff";
   36.20  
   36.21  AddIffs [converse_iff];
   36.22  
   36.23 -Goalw [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
   36.24 +Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
   36.25  by (Simp_tac 1);
   36.26  qed "converseI";
   36.27  
   36.28 -Goalw [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
   36.29 +Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
   36.30  by (Blast_tac 1);
   36.31  qed "converseD";
   36.32  
    37.1 --- a/src/HOL/Set.ML	Tue Jul 14 13:33:12 1998 +0200
    37.2 +++ b/src/HOL/Set.ML	Wed Jul 15 10:15:13 1998 +0200
    37.3 @@ -13,7 +13,7 @@
    37.4  Addsimps [Collect_mem_eq];
    37.5  AddIffs  [mem_Collect_eq];
    37.6  
    37.7 -Goal "!!a. P(a) ==> a : {x. P(x)}";
    37.8 +Goal "P(a) ==> a : {x. P(x)}";
    37.9  by (Asm_simp_tac 1);
   37.10  qed "CollectI";
   37.11  
   37.12 @@ -325,11 +325,11 @@
   37.13  
   37.14  Addsimps [Un_iff];
   37.15  
   37.16 -Goal "!!c. c:A ==> c : A Un B";
   37.17 +Goal "c:A ==> c : A Un B";
   37.18  by (Asm_simp_tac 1);
   37.19  qed "UnI1";
   37.20  
   37.21 -Goal "!!c. c:B ==> c : A Un B";
   37.22 +Goal "c:B ==> c : A Un B";
   37.23  by (Asm_simp_tac 1);
   37.24  qed "UnI2";
   37.25  
   37.26 @@ -356,15 +356,15 @@
   37.27  
   37.28  Addsimps [Int_iff];
   37.29  
   37.30 -Goal "!!c. [| c:A;  c:B |] ==> c : A Int B";
   37.31 +Goal "[| c:A;  c:B |] ==> c : A Int B";
   37.32  by (Asm_simp_tac 1);
   37.33  qed "IntI";
   37.34  
   37.35 -Goal "!!c. c : A Int B ==> c:A";
   37.36 +Goal "c : A Int B ==> c:A";
   37.37  by (Asm_full_simp_tac 1);
   37.38  qed "IntD1";
   37.39  
   37.40 -Goal "!!c. c : A Int B ==> c:B";
   37.41 +Goal "c : A Int B ==> c:B";
   37.42  by (Asm_full_simp_tac 1);
   37.43  qed "IntD2";
   37.44  
   37.45 @@ -436,7 +436,7 @@
   37.46  qed_goal "singletonI" Set.thy "a : {a}"
   37.47   (fn _=> [ (rtac insertI1 1) ]);
   37.48  
   37.49 -Goal "!!a. b : {a} ==> b=a";
   37.50 +Goal "b : {a} ==> b=a";
   37.51  by (Blast_tac 1);
   37.52  qed "singletonD";
   37.53  
   37.54 @@ -445,7 +445,7 @@
   37.55  qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
   37.56  (fn _ => [Blast_tac 1]);
   37.57  
   37.58 -Goal "!!a b. {a}={b} ==> a=b";
   37.59 +Goal "{a}={b} ==> a=b";
   37.60  by (blast_tac (claset() addEs [equalityE]) 1);
   37.61  qed "singleton_inject";
   37.62  
   37.63 @@ -469,7 +469,7 @@
   37.64  Addsimps [UN_iff];
   37.65  
   37.66  (*The order of the premises presupposes that A is rigid; b may be flexible*)
   37.67 -Goal "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
   37.68 +Goal "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
   37.69  by Auto_tac;
   37.70  qed "UN_I";
   37.71  
   37.72 @@ -504,7 +504,7 @@
   37.73  by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
   37.74  qed "INT_I";
   37.75  
   37.76 -Goal "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   37.77 +Goal "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   37.78  by Auto_tac;
   37.79  qed "INT_D";
   37.80  
   37.81 @@ -536,7 +536,7 @@
   37.82  Addsimps [Union_iff];
   37.83  
   37.84  (*The order of the premises presupposes that C is rigid; A may be flexible*)
   37.85 -Goal "!!X. [| X:C;  A:X |] ==> A : Union(C)";
   37.86 +Goal "[| X:C;  A:X |] ==> A : Union(C)";
   37.87  by Auto_tac;
   37.88  qed "UnionI";
   37.89  
   37.90 @@ -565,7 +565,7 @@
   37.91  
   37.92  (*A "destruct" rule -- every X in C contains A as an element, but
   37.93    A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   37.94 -Goal "!!X. [| A : Inter(C);  X:C |] ==> A:X";
   37.95 +Goal "[| A : Inter(C);  X:C |] ==> A:X";
   37.96  by Auto_tac;
   37.97  qed "InterD";
   37.98  
   37.99 @@ -626,7 +626,7 @@
  37.100  
  37.101  (*** Range of a function -- just a translation for image! ***)
  37.102  
  37.103 -Goal "!!b. b=f(x) ==> b : range(f)";
  37.104 +Goal "b=f(x) ==> b : range(f)";
  37.105  by (EVERY1 [etac image_eqI, rtac UNIV_I]);
  37.106  bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
  37.107  
    38.1 --- a/src/HOL/Sexp.ML	Tue Jul 14 13:33:12 1998 +0200
    38.2 +++ b/src/HOL/Sexp.ML	Wed Jul 15 10:15:13 1998 +0200
    38.3 @@ -124,7 +124,7 @@
    38.4  by (rtac sexp_case_Numb 1);
    38.5  qed "sexp_rec_Numb";
    38.6  
    38.7 -Goal "!!M. [| M: sexp;  N: sexp |] ==> \
    38.8 +Goal "[| M: sexp;  N: sexp |] ==> \
    38.9  \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
   38.10  by (rtac (sexp_rec_unfold RS trans) 1);
   38.11  by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
    39.1 --- a/src/HOL/Sum.ML	Tue Jul 14 13:33:12 1998 +0200
    39.2 +++ b/src/HOL/Sum.ML	Wed Jul 15 10:15:13 1998 +0200
    39.3 @@ -91,11 +91,11 @@
    39.4  
    39.5  (** Introduction rules for the injections **)
    39.6  
    39.7 -Goalw [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
    39.8 +Goalw [sum_def] "a : A ==> Inl(a) : A Plus B";
    39.9  by (Blast_tac 1);
   39.10  qed "InlI";
   39.11  
   39.12 -Goalw [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
   39.13 +Goalw [sum_def] "b : B ==> Inr(b) : A Plus B";
   39.14  by (Blast_tac 1);
   39.15  qed "InrI";
   39.16  
   39.17 @@ -189,13 +189,13 @@
   39.18  by (rtac Int_lower1 1);
   39.19  qed "Part_subset";
   39.20  
   39.21 -Goal "!!A B. A<=B ==> Part A h <= Part B h";
   39.22 +Goal "A<=B ==> Part A h <= Part B h";
   39.23  by (Blast_tac 1);
   39.24  qed "Part_mono";
   39.25  
   39.26  val basic_monos = basic_monos @ [Part_mono];
   39.27  
   39.28 -Goalw [Part_def] "!!a. a : Part A h ==> a : A";
   39.29 +Goalw [Part_def] "a : Part A h ==> a : A";
   39.30  by (etac IntD1 1);
   39.31  qed "PartD1";
   39.32  
    40.1 --- a/src/HOL/TLA/hypsubst.ML	Tue Jul 14 13:33:12 1998 +0200
    40.2 +++ b/src/HOL/TLA/hypsubst.ML	Wed Jul 15 10:15:13 1998 +0200
    40.3 @@ -17,10 +17,10 @@
    40.4  
    40.5  Test data:
    40.6  
    40.7 -Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
    40.8 -Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
    40.9 -Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
   40.10 -Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
   40.11 +Goal "[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
   40.12 +Goal "[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
   40.13 +Goal "[| ?x=y; P(?x) |] ==> y = a";
   40.14 +Goal "[| ?x=y; P(?x) |] ==> y = a";
   40.15  
   40.16  by (hyp_subst_tac 1);
   40.17  by (bound_hyp_subst_tac 1);
    41.1 --- a/src/HOL/Trancl.ML	Tue Jul 14 13:33:12 1998 +0200
    41.2 +++ b/src/HOL/Trancl.ML	Wed Jul 15 10:15:13 1998 +0200
    41.3 @@ -28,7 +28,7 @@
    41.4  
    41.5  
    41.6  (*Closure under composition with r*)
    41.7 -Goal "!!r. [| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
    41.8 +Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
    41.9  by (stac rtrancl_unfold 1);
   41.10  by (Blast_tac 1);
   41.11  qed "rtrancl_into_rtrancl";
   41.12 @@ -40,7 +40,7 @@
   41.13  qed "r_into_rtrancl";
   41.14  
   41.15  (*monotonicity of rtrancl*)
   41.16 -Goalw [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*";
   41.17 +Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
   41.18  by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
   41.19  qed "rtrancl_mono";
   41.20  
   41.21 @@ -120,19 +120,19 @@
   41.22  qed "rtrancl_idemp_self_comp";
   41.23  Addsimps [rtrancl_idemp_self_comp];
   41.24  
   41.25 -Goal "!!r s. r <= s^* ==> r^* <= s^*";
   41.26 +Goal "r <= s^* ==> r^* <= s^*";
   41.27  by (dtac rtrancl_mono 1);
   41.28  by (Asm_full_simp_tac 1);
   41.29  qed "rtrancl_subset_rtrancl";
   41.30  
   41.31 -Goal "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
   41.32 +Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
   41.33  by (dtac rtrancl_mono 1);
   41.34  by (dtac rtrancl_mono 1);
   41.35  by (Asm_full_simp_tac 1);
   41.36  by (Blast_tac 1);
   41.37  qed "rtrancl_subset";
   41.38  
   41.39 -Goal "!!R. (R^* Un S^*)^* = (R Un S)^*";
   41.40 +Goal "(R^* Un S^*)^* = (R Un S)^*";
   41.41  by (blast_tac (claset() addSIs [rtrancl_subset]
   41.42                         addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   41.43  qed "rtrancl_Un_rtrancl";
   41.44 @@ -143,14 +143,14 @@
   41.45  qed "rtrancl_reflcl";
   41.46  Addsimps [rtrancl_reflcl];
   41.47  
   41.48 -Goal "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
   41.49 +Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
   41.50  by (rtac converseI 1);
   41.51  by (etac rtrancl_induct 1);
   41.52  by (rtac rtrancl_refl 1);
   41.53  by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
   41.54  qed "rtrancl_converseD";
   41.55  
   41.56 -Goal "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
   41.57 +Goal "(x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
   41.58  by (dtac converseD 1);
   41.59  by (etac rtrancl_induct 1);
   41.60  by (rtac rtrancl_refl 1);
   41.61 @@ -204,7 +204,7 @@
   41.62  
   41.63  (**** The relation trancl ****)
   41.64  
   41.65 -Goalw [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
   41.66 +Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
   41.67  by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
   41.68  qed "trancl_mono";
   41.69  
    42.1 --- a/src/HOL/Univ.ML	Tue Jul 14 13:33:12 1998 +0200
    42.2 +++ b/src/HOL/Univ.ML	Wed Jul 15 10:15:13 1998 +0200
    42.3 @@ -142,11 +142,11 @@
    42.4  
    42.5  (** Injectiveness of Scons **)
    42.6  
    42.7 -Goalw [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
    42.8 +Goalw [Scons_def] "M$N <= M'$N' ==> M<=M'";
    42.9  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
   42.10  qed "Scons_inject_lemma1";
   42.11  
   42.12 -Goalw [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
   42.13 +Goalw [Scons_def] "M$N <= M'$N' ==> N<=N'";
   42.14  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
   42.15  qed "Scons_inject_lemma2";
   42.16  
   42.17 @@ -297,7 +297,7 @@
   42.18  
   42.19  (*** Cartesian Product ***)
   42.20  
   42.21 -Goalw [uprod_def] "!!M N. [| M:A;  N:B |] ==> (M$N) : A<*>B";
   42.22 +Goalw [uprod_def] "[| M:A;  N:B |] ==> (M$N) : A<*>B";
   42.23  by (REPEAT (ares_tac [singletonI,UN_I] 1));
   42.24  qed "uprodI";
   42.25  
   42.26 @@ -322,11 +322,11 @@
   42.27  
   42.28  (*** Disjoint Sum ***)
   42.29  
   42.30 -Goalw [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
   42.31 +Goalw [usum_def] "M:A ==> In0(M) : A<+>B";
   42.32  by (Blast_tac 1);
   42.33  qed "usum_In0I";
   42.34  
   42.35 -Goalw [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
   42.36 +Goalw [usum_def] "N:B ==> In1(N) : A<+>B";
   42.37  by (Blast_tac 1);
   42.38  qed "usum_In1I";
   42.39  
   42.40 @@ -408,23 +408,23 @@
   42.41  
   42.42  (*** Monotonicity ***)
   42.43  
   42.44 -Goalw [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
   42.45 +Goalw [uprod_def] "[| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
   42.46  by (Blast_tac 1);
   42.47  qed "uprod_mono";
   42.48  
   42.49 -Goalw [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
   42.50 +Goalw [usum_def] "[| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
   42.51  by (Blast_tac 1);
   42.52  qed "usum_mono";
   42.53  
   42.54 -Goalw [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
   42.55 +Goalw [Scons_def] "[| M<=M';  N<=N' |] ==> M$N <= M'$N'";
   42.56  by (Blast_tac 1);
   42.57  qed "Scons_mono";
   42.58  
   42.59 -Goalw [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
   42.60 +Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)";
   42.61  by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
   42.62  qed "In0_mono";
   42.63  
   42.64 -Goalw [In1_def] "!!M N. M<=N ==> In1(M) <= In1(N)";
   42.65 +Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)";
   42.66  by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
   42.67  qed "In1_mono";
   42.68  
   42.69 @@ -471,7 +471,7 @@
   42.70  
   42.71  (*** Equality : the diagonal relation ***)
   42.72  
   42.73 -Goalw [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
   42.74 +Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
   42.75  by (Blast_tac 1);
   42.76  qed "diag_eqI";
   42.77  
   42.78 @@ -506,11 +506,11 @@
   42.79  
   42.80  (*** Equality for Disjoint Sum ***)
   42.81  
   42.82 -Goalw [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
   42.83 +Goalw [dsum_def]  "(M,M'):r ==> (In0(M), In0(M')) : r<++>s";
   42.84  by (Blast_tac 1);
   42.85  qed "dsum_In0I";
   42.86  
   42.87 -Goalw [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
   42.88 +Goalw [dsum_def]  "(N,N'):s ==> (In1(N), In1(N')) : r<++>s";
   42.89  by (Blast_tac 1);
   42.90  qed "dsum_In1I";
   42.91  
   42.92 @@ -531,11 +531,11 @@
   42.93  
   42.94  (*** Monotonicity ***)
   42.95  
   42.96 -Goal "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
   42.97 +Goal "[| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
   42.98  by (Blast_tac 1);
   42.99  qed "dprod_mono";
  42.100  
  42.101 -Goal "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
  42.102 +Goal "[| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
  42.103  by (Blast_tac 1);
  42.104  qed "dsum_mono";
  42.105  
    43.1 --- a/src/HOL/Vimage.ML	Tue Jul 14 13:33:12 1998 +0200
    43.2 +++ b/src/HOL/Vimage.ML	Wed Jul 15 10:15:13 1998 +0200
    43.3 @@ -102,6 +102,6 @@
    43.4  
    43.5  (** monotonicity **)
    43.6  
    43.7 -Goal "!!f. A<=B ==> f-``A <= f-``B";
    43.8 +Goal "A<=B ==> f-``A <= f-``B";
    43.9  by (Blast_tac 1);
   43.10  qed "vimage_mono";
    44.1 --- a/src/HOL/W0/MiniML.ML	Tue Jul 14 13:33:12 1998 +0200
    44.2 +++ b/src/HOL/W0/MiniML.ML	Wed Jul 15 10:15:13 1998 +0200
    44.3 @@ -11,7 +11,7 @@
    44.4  
    44.5  
    44.6  (* has_type is closed w.r.t. substitution *)
    44.7 -Goal "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
    44.8 +Goal "a |- e :: t ==> $s a |- e :: $s t";
    44.9  by (etac has_type.induct 1);
   44.10  (* case VarI *)
   44.11  by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
    45.1 --- a/src/HOL/WF.ML	Tue Jul 14 13:33:12 1998 +0200
    45.2 +++ b/src/HOL/WF.ML	Wed Jul 15 10:15:13 1998 +0200
    45.3 @@ -93,7 +93,7 @@
    45.4   * Wellfoundedness of subsets
    45.5   *---------------------------------------------------------------------------*)
    45.6  
    45.7 -Goal "!!r. [| wf(r);  p<=r |] ==> wf(p)";
    45.8 +Goal "[| wf(r);  p<=r |] ==> wf(p)";
    45.9  by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
   45.10  by (Fast_tac 1);
   45.11  qed "wf_subset";
   45.12 @@ -164,7 +164,7 @@
   45.13  by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
   45.14  qed "cuts_eq";
   45.15  
   45.16 -Goalw [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   45.17 +Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)";
   45.18  by (asm_simp_tac HOL_ss 1);
   45.19  qed "cut_apply";
   45.20  
    46.1 --- a/src/HOL/WF_Rel.ML	Tue Jul 14 13:33:12 1998 +0200
    46.2 +++ b/src/HOL/WF_Rel.ML	Wed Jul 15 10:15:13 1998 +0200
    46.3 @@ -32,7 +32,7 @@
    46.4   * The inverse image into a wellfounded relation is wellfounded.
    46.5   *---------------------------------------------------------------------------*)
    46.6  
    46.7 -Goal "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
    46.8 +Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
    46.9  by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
   46.10  by (Clarify_tac 1);
   46.11  by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
   46.12 @@ -110,7 +110,7 @@
   46.13   * Cannot go into WF because it needs Finite
   46.14   *---------------------------------------------------------------------------*)
   46.15  
   46.16 -Goal "!!r. finite r ==> acyclic r --> wf r";
   46.17 +Goal "finite r ==> acyclic r --> wf r";
   46.18  by (etac finite_induct 1);
   46.19   by (Blast_tac 1);
   46.20  by (split_all_tac 1);
   46.21 @@ -122,7 +122,7 @@
   46.22  	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
   46.23  	etac (acyclic_converse RS iffD2) 1]);
   46.24  
   46.25 -Goal "!!r. finite r ==> wf r = acyclic r";
   46.26 +Goal "finite r ==> wf r = acyclic r";
   46.27  by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
   46.28  qed "wf_iff_acyclic_if_finite";
   46.29  
    47.1 --- a/src/HOL/equalities.ML	Tue Jul 14 13:33:12 1998 +0200
    47.2 +++ b/src/HOL/equalities.ML	Wed Jul 15 10:15:13 1998 +0200
    47.3 @@ -51,7 +51,7 @@
    47.4  bind_thm("empty_not_insert",insert_not_empty RS not_sym);
    47.5  Addsimps[empty_not_insert];
    47.6  
    47.7 -Goal "!!a. a:A ==> insert a A = A";
    47.8 +Goal "a:A ==> insert a A = A";
    47.9  by (Blast_tac 1);
   47.10  qed "insert_absorb";
   47.11  (* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
   47.12 @@ -72,12 +72,12 @@
   47.13  qed "insert_subset";
   47.14  Addsimps[insert_subset];
   47.15  
   47.16 -Goal "!!a. insert a A ~= insert a B ==> A ~= B";
   47.17 +Goal "insert a A ~= insert a B ==> A ~= B";
   47.18  by (Blast_tac 1);
   47.19  qed "insert_lim";
   47.20  
   47.21  (* use new B rather than (A-{a}) to avoid infinite unfolding *)
   47.22 -Goal "!!a. a:A ==> ? B. A = insert a B & a ~: B";
   47.23 +Goal "a:A ==> ? B. A = insert a B & a ~: B";
   47.24  by (res_inst_tac [("x","A-{a}")] exI 1);
   47.25  by (Blast_tac 1);
   47.26  qed "mk_disjoint_insert";
   47.27 @@ -114,7 +114,7 @@
   47.28  by (Blast_tac 1);
   47.29  qed "image_image";
   47.30  
   47.31 -Goal "!!x. x:A ==> insert (f x) (f``A) = f``A";
   47.32 +Goal "x:A ==> insert (f x) (f``A) = f``A";
   47.33  by (Blast_tac 1);
   47.34  qed "insert_image";
   47.35  Addsimps [insert_image];
   47.36 @@ -164,11 +164,11 @@
   47.37  (*Intersection is an AC-operator*)
   47.38  val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
   47.39  
   47.40 -Goal "!!A B. B<=A ==> A Int B = B";
   47.41 +Goal "B<=A ==> A Int B = B";
   47.42  by (Blast_tac 1);
   47.43  qed "Int_absorb1";
   47.44  
   47.45 -Goal "!!A B. A<=B ==> A Int B = A";
   47.46 +Goal "A<=B ==> A Int B = A";
   47.47  by (Blast_tac 1);
   47.48  qed "Int_absorb2";
   47.49  
   47.50 @@ -243,11 +243,11 @@
   47.51  (*Union is an AC-operator*)
   47.52  val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
   47.53  
   47.54 -Goal "!!A B. A<=B ==> A Un B = B";
   47.55 +Goal "A<=B ==> A Un B = B";
   47.56  by (Blast_tac 1);
   47.57  qed "Un_absorb1";
   47.58  
   47.59 -Goal "!!A B. B<=A ==> A Un B = A";
   47.60 +Goal "B<=A ==> A Un B = A";
   47.61  by (Blast_tac 1);
   47.62  qed "Un_absorb2";
   47.63  
   47.64 @@ -446,7 +446,7 @@
   47.65  qed "UN_singleton";
   47.66  Addsimps [UN_singleton];
   47.67  
   47.68 -Goal "!!k. k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
   47.69 +Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
   47.70  by (Blast_tac 1);
   47.71  qed "UN_absorb";
   47.72  
   47.73 @@ -455,7 +455,7 @@
   47.74  qed "INT_empty";
   47.75  Addsimps[INT_empty];
   47.76  
   47.77 -Goal "!!k. k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
   47.78 +Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
   47.79  by (Blast_tac 1);
   47.80  qed "INT_absorb";
   47.81  
   47.82 @@ -490,12 +490,12 @@
   47.83  by (Blast_tac 1);
   47.84  qed "Inter_image_eq";
   47.85  
   47.86 -Goal "!!A. A~={} ==> (UN y:A. c) = c";
   47.87 +Goal "A~={} ==> (UN y:A. c) = c";
   47.88  by (Blast_tac 1);
   47.89  qed "UN_constant";
   47.90  Addsimps[UN_constant];
   47.91  
   47.92 -Goal "!!A. A~={} ==> (INT y:A. c) = c";
   47.93 +Goal "A~={} ==> (INT y:A. c) = c";
   47.94  by (Blast_tac 1);
   47.95  qed "INT_constant";
   47.96  Addsimps[INT_constant];
   47.97 @@ -601,7 +601,7 @@
   47.98  qed "Diff_cancel";
   47.99  Addsimps[Diff_cancel];
  47.100  
  47.101 -Goal "!!A B. A Int B = {} ==> A-B = A";
  47.102 +Goal "A Int B = {} ==> A-B = A";
  47.103  by (blast_tac (claset() addEs [equalityE]) 1);
  47.104  qed "Diff_triv";
  47.105  
  47.106 @@ -620,7 +620,7 @@
  47.107  qed "Diff_UNIV";
  47.108  Addsimps[Diff_UNIV];
  47.109  
  47.110 -Goal "!!x. x~:A ==> A - insert x B = A-B";
  47.111 +Goal "x~:A ==> A - insert x B = A-B";
  47.112  by (Blast_tac 1);
  47.113  qed "Diff_insert0";
  47.114  Addsimps [Diff_insert0];
  47.115 @@ -640,12 +640,12 @@
  47.116  by (Blast_tac 1);
  47.117  qed "insert_Diff_if";
  47.118  
  47.119 -Goal "!!x. x:B ==> insert x A - B = A-B";
  47.120 +Goal "x:B ==> insert x A - B = A-B";
  47.121  by (Blast_tac 1);
  47.122  qed "insert_Diff1";
  47.123  Addsimps [insert_Diff1];
  47.124  
  47.125 -Goal "!!a. a:A ==> insert a (A-{a}) = A";
  47.126 +Goal "a:A ==> insert a (A-{a}) = A";
  47.127  by (Blast_tac 1);
  47.128  qed "insert_Diff";
  47.129  
  47.130 @@ -654,11 +654,11 @@
  47.131  qed "Diff_disjoint";
  47.132  Addsimps[Diff_disjoint];
  47.133  
  47.134 -Goal "!!A. A<=B ==> A Un (B-A) = B";
  47.135 +Goal "A<=B ==> A Un (B-A) = B";
  47.136  by (Blast_tac 1);
  47.137  qed "Diff_partition";
  47.138  
  47.139 -Goal "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
  47.140 +Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
  47.141  by (Blast_tac 1);
  47.142  qed "double_diff";
  47.143  
    48.1 --- a/src/HOL/ex/Fib.ML	Tue Jul 14 13:33:12 1998 +0200
    48.2 +++ b/src/HOL/ex/Fib.ML	Wed Jul 15 10:15:13 1998 +0200
    48.3 @@ -45,7 +45,7 @@
    48.4  (* Also add  0 < fib (Suc n) *)
    48.5  Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
    48.6  
    48.7 -Goal "!!n. 0<n ==> 0 < fib n";
    48.8 +Goal "0<n ==> 0 < fib n";
    48.9  by (rtac (not0_implies_Suc RS exE) 1);
   48.10  by Auto_tac;
   48.11  qed "fib_gr_0";
   48.12 @@ -93,12 +93,12 @@
   48.13  by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
   48.14  qed "gcd_fib_add";
   48.15  
   48.16 -Goal "!!m. m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
   48.17 +Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
   48.18  by (rtac (gcd_fib_add RS sym RS trans) 1);
   48.19  by (Asm_simp_tac 1);
   48.20  qed "gcd_fib_diff";
   48.21  
   48.22 -Goal "!!m. 0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
   48.23 +Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
   48.24  by (res_inst_tac [("n","n")] less_induct 1);
   48.25  by (stac mod_if 1);
   48.26  by (Asm_simp_tac 1);
    49.1 --- a/src/HOL/ex/InSort.ML	Tue Jul 14 13:33:12 1998 +0200
    49.2 +++ b/src/HOL/ex/InSort.ML	Wed Jul 15 10:15:13 1998 +0200
    49.3 @@ -32,7 +32,7 @@
    49.4  qed "sorted_ins";
    49.5  Addsimps [sorted_ins];
    49.6  
    49.7 -Goal "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
    49.8 +Goal "[| total(f); transf(f) |] ==>  sorted f (insort f xs)";
    49.9  by (list.induct_tac "xs" 1);
   49.10  by (ALLGOALS Asm_simp_tac);
   49.11  qed "sorted_insort";
    50.1 --- a/src/HOL/ex/MT.ML	Tue Jul 14 13:33:12 1998 +0200
    50.2 +++ b/src/HOL/ex/MT.ML	Wed Jul 15 10:15:13 1998 +0200
    50.3 @@ -574,7 +574,7 @@
    50.4  
    50.5  (* Introduction rules for hasty *)
    50.6  
    50.7 -Goalw [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
    50.8 +Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
    50.9  by (etac hasty_rel_const_coind 1);
   50.10  qed "hasty_const";
   50.11  
   50.12 @@ -592,7 +592,7 @@
   50.13  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
   50.14  qed "hasty_elim_const_lem";
   50.15  
   50.16 -Goal "!!c. v_const(c) hasty t ==> c isof t";
   50.17 +Goal "v_const(c) hasty t ==> c isof t";
   50.18  by (dtac hasty_elim_const_lem 1);
   50.19  by (Blast_tac 1);
   50.20  qed "hasty_elim_const";
    51.1 --- a/src/HOL/ex/Primes.ML	Tue Jul 14 13:33:12 1998 +0200
    51.2 +++ b/src/HOL/ex/Primes.ML	Wed Jul 15 10:15:13 1998 +0200
    51.3 @@ -46,7 +46,7 @@
    51.4  qed "gcd_0";
    51.5  Addsimps [gcd_0];
    51.6  
    51.7 -Goal "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
    51.8 +Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
    51.9  by (rtac (gcd_eq RS trans) 1);
   51.10  by (Asm_simp_tac 1);
   51.11  by (Blast_tac 1);
   51.12 @@ -71,7 +71,7 @@
   51.13  
   51.14  (*Maximality: for all m,n,f naturals, 
   51.15                  if f divides m and f divides n then f divides gcd(m,n)*)
   51.16 -Goal "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
   51.17 +Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
   51.18  by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
   51.19  by (ALLGOALS
   51.20      (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod,
   51.21 @@ -84,7 +84,7 @@
   51.22  qed "is_gcd";
   51.23  
   51.24  (*uniqueness of GCDs*)
   51.25 -Goalw [is_gcd_def] "!!m n. [| is_gcd m a b; is_gcd n a b |] ==> m=n";
   51.26 +Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n";
   51.27  by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
   51.28  qed "is_gcd_unique";
   51.29  
   51.30 @@ -150,20 +150,20 @@
   51.31  qed "gcd_mult";
   51.32  Addsimps [gcd_mult];
   51.33  
   51.34 -Goal "!!k. [| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
   51.35 +Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
   51.36  by (subgoal_tac "m = gcd(m*k, m*n)" 1);
   51.37  by (etac ssubst 1 THEN rtac gcd_greatest 1);
   51.38  by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
   51.39  qed "relprime_dvd_mult";
   51.40  
   51.41 -Goalw [prime_def] "!!p. [| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
   51.42 +Goalw [prime_def] "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
   51.43  by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
   51.44 -by (fast_tac (claset() addss (simpset())) 1);
   51.45 +by Auto_tac;
   51.46  qed "prime_imp_relprime";
   51.47  
   51.48  (*This theorem leads immediately to a proof of the uniqueness of factorization.
   51.49    If p divides a product of primes then it is one of those primes.*)
   51.50 -Goal "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
   51.51 +Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
   51.52  by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1);
   51.53  qed "prime_dvd_mult";
   51.54  
   51.55 @@ -192,7 +192,7 @@
   51.56                                 gcd_dvd1, gcd_dvd2]) 1);
   51.57  qed "gcd_dvd_gcd_mult";
   51.58  
   51.59 -Goal "!!n. gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
   51.60 +Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
   51.61  by (rtac dvd_anti_sym 1);
   51.62  by (rtac gcd_dvd_gcd_mult 2);
   51.63  by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1);
    52.1 --- a/src/HOL/ex/Primrec.ML	Tue Jul 14 13:33:12 1998 +0200
    52.2 +++ b/src/HOL/ex/Primrec.ML	Wed Jul 15 10:15:13 1998 +0200
    52.3 @@ -71,7 +71,7 @@
    52.4  qed_spec_mp "ack_less_mono2";
    52.5  
    52.6  (*PROPERTY A 5', monotonicity for<=*)
    52.7 -Goal "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)";
    52.8 +Goal "j<=k ==> ack(i,j)<=ack(i,k)";
    52.9  by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
   52.10  by (blast_tac (claset() addIs [ack_less_mono2]) 1);
   52.11  qed "ack_le_mono2";
   52.12 @@ -127,13 +127,13 @@
   52.13  by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
   52.14  val lemma = result();
   52.15  
   52.16 -Goal "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
   52.17 +Goal "i<j ==> ack(i,k) < ack(j,k)";
   52.18  by (dtac less_eq_Suc_add 1);
   52.19  by (blast_tac (claset() addSIs [lemma]) 1);
   52.20  qed "ack_less_mono1";
   52.21  
   52.22  (*PROPERTY A 7', monotonicity for<=*)
   52.23 -Goal "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)";
   52.24 +Goal "i<=j ==> ack(i,k)<=ack(j,k)";
   52.25  by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
   52.26  by (blast_tac (claset() addIs [ack_less_mono1]) 1);
   52.27  qed "ack_le_mono1";
   52.28 @@ -160,7 +160,7 @@
   52.29  
   52.30  (*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   52.31    used k+4.  Quantified version must be nested EX k'. ALL i,j... *)
   52.32 -Goal "!!i j k. i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
   52.33 +Goal "i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
   52.34  by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1);
   52.35  by (rtac (ack_add_bound RS less_le_trans) 2);
   52.36  by (Asm_simp_tac 2);
   52.37 @@ -254,7 +254,7 @@
   52.38  by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1));
   52.39  qed "PREC_case";
   52.40  
   52.41 -Goal "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
   52.42 +Goal "f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
   52.43  by (etac PRIMREC.induct 1);
   52.44  by (ALLGOALS 
   52.45      (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
    53.1 --- a/src/HOLCF/Fix.ML	Tue Jul 14 13:33:12 1998 +0200
    53.2 +++ b/src/HOLCF/Fix.ML	Wed Jul 15 10:15:13 1998 +0200
    53.3 @@ -884,7 +884,7 @@
    53.4          (Simp_tac 1)
    53.5          ]);
    53.6  
    53.7 -Goal "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
    53.8 +Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
    53.9  \           ==> adm (%x. P x = Q x)";
   53.10  by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
   53.11  by (Asm_simp_tac 1);
    54.1 --- a/src/HOLCF/IMP/Denotational.ML	Tue Jul 14 13:33:12 1998 +0200
    54.2 +++ b/src/HOLCF/IMP/Denotational.ML	Wed Jul 15 10:15:13 1998 +0200
    54.3 @@ -22,7 +22,7 @@
    54.4  qed "dlift_is_Def";
    54.5  Addsimps [dlift_is_Def];
    54.6  
    54.7 -Goal "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
    54.8 +Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
    54.9  by (etac evalc.induct 1);
   54.10        by (ALLGOALS Asm_simp_tac);
   54.11   by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
    55.1 --- a/src/HOLCF/Lift.ML	Tue Jul 14 13:33:12 1998 +0200
    55.2 +++ b/src/HOLCF/Lift.ML	Wed Jul 15 10:15:13 1998 +0200
    55.3 @@ -36,9 +36,7 @@
    55.4  
    55.5  Goal "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
    55.6  \   cont (%y. lift_case UU (f y) (g y))";
    55.7 -by (rtac cont2cont_app 1);
    55.8 -back();
    55.9 -by (safe_tac set_cs);
   55.10 +by (res_inst_tac [("tt","g")] cont2cont_app 1);
   55.11  by (rtac cont_flift1_not_arg 1);
   55.12  by Auto_tac;
   55.13  by (rtac cont_flift1_arg 1);
   55.14 @@ -100,7 +98,7 @@
   55.15  
   55.16  Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
   55.17  
   55.18 -Goal "!!x. x~=UU ==> (flift2 f)`x~=UU";
   55.19 +Goal "x~=UU ==> (flift2 f)`x~=UU";
   55.20  by (def_tac 1);
   55.21  qed"flift2_nUU";
   55.22  
    56.1 --- a/src/HOLCF/Lift2.ML	Tue Jul 14 13:33:12 1998 +0200
    56.2 +++ b/src/HOLCF/Lift2.ML	Wed Jul 15 10:15:13 1998 +0200
    56.3 @@ -44,7 +44,7 @@
    56.4  
    56.5  (* Tailoring notUU_I of Pcpo.ML to Undef *)
    56.6  
    56.7 -Goal "!!x. [| x<<y; ~x=Undef |] ==> ~y=Undef";
    56.8 +Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
    56.9  by (etac contrapos 1);
   56.10  by (hyp_subst_tac 1);
   56.11  by (rtac antisym_less 1);
    57.1 --- a/src/HOLCF/Lift3.ML	Tue Jul 14 13:33:12 1998 +0200
    57.2 +++ b/src/HOLCF/Lift3.ML	Wed Jul 15 10:15:13 1998 +0200
    57.3 @@ -139,13 +139,13 @@
    57.4  
    57.5  (* Two specific lemmas for the combination of LCF and HOL terms *)
    57.6  
    57.7 -Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
    57.8 +Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
    57.9  by (rtac cont2cont_CF1L 1);
   57.10  by (REPEAT (resolve_tac cont_lemmas1 1));
   57.11  by Auto_tac;
   57.12  qed"cont_fapp_app";
   57.13  
   57.14 -Goal "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
   57.15 +Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
   57.16  by (rtac cont2cont_CF1L 1);
   57.17  by (etac cont_fapp_app 1);
   57.18  by (assume_tac 1);
    58.1 --- a/src/HOLCF/Tr.ML	Tue Jul 14 13:33:12 1998 +0200
    58.2 +++ b/src/HOLCF/Tr.ML	Wed Jul 15 10:15:13 1998 +0200
    58.3 @@ -120,7 +120,7 @@
    58.4  by Auto_tac;
    58.5  qed"andalso_or";
    58.6  
    58.7 -Goal "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
    58.8 +Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
    58.9  by (rtac iffI 1);
   58.10  by (res_inst_tac [("p","t")] trE 1);
   58.11  by Auto_tac;
   58.12 @@ -176,12 +176,12 @@
   58.13  val adm_tricks = [adm_trick_1,adm_trick_2];
   58.14  
   58.15  
   58.16 -Goal "!!f. cont(f) ==> adm (%x. (f x)~=TT)";
   58.17 +Goal "cont(f) ==> adm (%x. (f x)~=TT)";
   58.18  by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
   58.19  by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
   58.20  qed"adm_nTT";
   58.21  
   58.22 -Goal "!!f. cont(f) ==> adm (%x. (f x)~=FF)";
   58.23 +Goal "cont(f) ==> adm (%x. (f x)~=FF)";
   58.24  by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
   58.25  by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
   58.26  qed"adm_nFF";
    59.1 --- a/src/ZF/Cardinal.ML	Tue Jul 14 13:33:12 1998 +0200
    59.2 +++ b/src/ZF/Cardinal.ML	Wed Jul 15 10:15:13 1998 +0200
    59.3 @@ -257,7 +257,7 @@
    59.4  
    59.5  (*Need AC to get X lepoll Y ==> |X| le |Y|;  see well_ord_lepoll_imp_Card_le
    59.6    Converse also requires AC, but see well_ord_cardinal_eqE*)
    59.7 -Goalw [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
    59.8 +Goalw [eqpoll_def,cardinal_def] "X eqpoll Y ==> |X| = |Y|";
    59.9  by (rtac Least_cong 1);
   59.10  by (blast_tac (claset() addIs [comp_bij, bij_converse_bij]) 1);
   59.11  qed "cardinal_cong";
    60.1 --- a/src/ZF/Coind/Map.ML	Tue Jul 14 13:33:12 1998 +0200
    60.2 +++ b/src/ZF/Coind/Map.ML	Wed Jul 15 10:15:13 1998 +0200
    60.3 @@ -82,7 +82,7 @@
    60.4  (* Monotonicity                                                 *)
    60.5  (* ############################################################ *)
    60.6  
    60.7 -Goalw [PMap_def,TMap_def] "!!A. B<=C ==> PMap(A,B)<=PMap(A,C)";
    60.8 +Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
    60.9  by (Fast_tac 1);
   60.10  qed "map_mono";
   60.11  
    61.1 --- a/src/ZF/Ordinal.ML	Tue Jul 14 13:33:12 1998 +0200
    61.2 +++ b/src/ZF/Ordinal.ML	Wed Jul 15 10:15:13 1998 +0200
    61.3 @@ -103,7 +103,7 @@
    61.4  
    61.5  (*** Lemmas for ordinals ***)
    61.6  
    61.7 -Goalw [Ord_def,Transset_def] "!!i j.[| Ord(i);  j:i |] ==> Ord(j)";
    61.8 +Goalw [Ord_def,Transset_def] "[| Ord(i);  j:i |] ==> Ord(j)";
    61.9  by (Blast_tac 1);
   61.10  qed "Ord_in_Ord";
   61.11  
   61.12 @@ -117,7 +117,7 @@
   61.13       ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
   61.14  qed "Ord_subset_Ord";
   61.15  
   61.16 -Goalw [Ord_def,Transset_def] "!!i j. [| j:i;  Ord(i) |] ==> j<=i";
   61.17 +Goalw [Ord_def,Transset_def] "[| j:i;  Ord(i) |] ==> j<=i";
   61.18  by (Blast_tac 1);
   61.19  qed "OrdmemD";
   61.20  
    62.1 --- a/src/ZF/Perm.ML	Tue Jul 14 13:33:12 1998 +0200
    62.2 +++ b/src/ZF/Perm.ML	Wed Jul 15 10:15:13 1998 +0200
    62.3 @@ -133,7 +133,7 @@
    62.4  by (rtac (prem RS lam_mono) 1);
    62.5  qed "id_mono";
    62.6  
    62.7 -Goalw [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)";
    62.8 +Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
    62.9  by (REPEAT (ares_tac [CollectI,lam_type] 1));
   62.10  by (etac subsetD 1 THEN assume_tac 1);
   62.11  by (Simp_tac 1);