More tidying and removal of "\!\!... from Goal commands
authorpaulson
Wed Jul 15 14:19:02 1998 +0200 (1998-07-15)
changeset 514874919e8f221c
parent 5147 825877190618
child 5149 10f0be29c0d1
More tidying and removal of "\!\!... from Goal commands
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Gfp.ML
src/HOL/IOA/IOA.ML
src/HOL/Induct/Comb.ML
src/HOL/Induct/Exp.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/SList.ML
src/HOL/Induct/Simult.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Integ.ML
src/HOL/NatDef.ML
src/HOL/Real/Lubs.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/Real.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/W0/Type.ML
src/HOL/W0/W.ML
src/HOL/WF.ML
src/HOL/equalities.ML
src/HOL/ex/MT.ML
src/HOL/ex/Primes.ML
src/HOL/ex/Primrec.ML
src/HOL/ex/Qsort.ML
     1.1 --- a/src/HOL/Finite.ML	Wed Jul 15 14:13:18 1998 +0200
     1.2 +++ b/src/HOL/Finite.ML	Wed Jul 15 14:19:02 1998 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  (** Sigma of finite sets **)
     1.5  
     1.6  Goalw [Sigma_def]
     1.7 - "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
     1.8 + "[| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
     1.9  by (blast_tac (claset() addSIs [finite_UnionI]) 1);
    1.10  bind_thm("finite_SigmaI", ballI RSN (2,result()));
    1.11  Addsimps [finite_SigmaI];
    1.12 @@ -212,7 +212,7 @@
    1.13  qed "finite_has_card";
    1.14  
    1.15  Goal
    1.16 -  "!!A.[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
    1.17 +  "[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
    1.18  \  ? m::nat. m<n & (? g. A = {g i|i. i<m})";
    1.19  by (res_inst_tac [("n","n")] natE 1);
    1.20   by (hyp_subst_tac 1);
    1.21 @@ -303,7 +303,7 @@
    1.22  val lemma = result();
    1.23  
    1.24  Goalw [card_def]
    1.25 -  "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
    1.26 +  "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
    1.27  by (etac lemma 1);
    1.28  by (assume_tac 1);
    1.29  qed "card_insert_disjoint";
    1.30 @@ -396,8 +396,7 @@
    1.31  
    1.32  
    1.33  (*Proper subsets*)
    1.34 -Goalw [psubset_def]
    1.35 -    "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
    1.36 +Goalw [psubset_def] "finite B ==> !A. A < B --> card(A) < card(B)";
    1.37  by (etac finite_induct 1);
    1.38  by (Simp_tac 1);
    1.39  by (Clarify_tac 1);
     2.1 --- a/src/HOL/Fun.ML	Wed Jul 15 14:13:18 1998 +0200
     2.2 +++ b/src/HOL/Fun.ML	Wed Jul 15 14:19:02 1998 +0200
     2.3 @@ -109,7 +109,7 @@
     2.4  qed "inj_on_contraD";
     2.5  
     2.6  Goalw [inj_on_def]
     2.7 -    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
     2.8 +    "[| A<=B; inj_on f B |] ==> inj_on f A";
     2.9  by (Blast_tac 1);
    2.10  qed "subset_inj_on";
    2.11  
    2.12 @@ -117,7 +117,7 @@
    2.13  (*** Lemmas about inj ***)
    2.14  
    2.15  Goalw [o_def]
    2.16 -    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    2.17 +    "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
    2.18  by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
    2.19  qed "comp_inj";
    2.20  
    2.21 @@ -141,12 +141,12 @@
    2.22  qed "inj_on_inv";
    2.23  
    2.24  Goalw [inj_on_def]
    2.25 -   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    2.26 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
    2.27  by (Blast_tac 1);
    2.28  qed "inj_on_image_Int";
    2.29  
    2.30  Goalw [inj_on_def]
    2.31 -   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
    2.32 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
    2.33  by (Blast_tac 1);
    2.34  qed "inj_on_image_set_diff";
    2.35  
     3.1 --- a/src/HOL/Gfp.ML	Wed Jul 15 14:13:18 1998 +0200
     3.2 +++ b/src/HOL/Gfp.ML	Wed Jul 15 14:19:02 1998 +0200
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1993  University of Cambridge
     3.6  
     3.7 -For gfp.thy.  The Knaster-Tarski Theorem for greatest fixed points.
     3.8 +The Knaster-Tarski Theorem for greatest fixed points.
     3.9  *)
    3.10  
    3.11  open Gfp;
    3.12 @@ -12,9 +12,8 @@
    3.13  
    3.14  (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
    3.15  
    3.16 -val prems = goalw Gfp.thy [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
    3.17 -by (rtac (CollectI RS Union_upper) 1);
    3.18 -by (resolve_tac prems 1);
    3.19 +Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
    3.20 +by (etac (CollectI RS Union_upper) 1);
    3.21  qed "gfp_upperbound";
    3.22  
    3.23  val prems = goalw Gfp.thy [gfp_def]
    3.24 @@ -40,10 +39,9 @@
    3.25  (*** Coinduction rules for greatest fixed points ***)
    3.26  
    3.27  (*weak version*)
    3.28 -val prems = goal Gfp.thy
    3.29 -    "[| a: X;  X <= f(X) |] ==> a : gfp(f)";
    3.30 +Goal "[| a: X;  X <= f(X) |] ==> a : gfp(f)";
    3.31  by (rtac (gfp_upperbound RS subsetD) 1);
    3.32 -by (REPEAT (ares_tac prems 1));
    3.33 +by Auto_tac;
    3.34  qed "weak_coinduct";
    3.35  
    3.36  val [prem,mono] = goal Gfp.thy
    3.37 @@ -56,8 +54,7 @@
    3.38  qed "coinduct_lemma";
    3.39  
    3.40  (*strong version, thanks to Coen & Frost*)
    3.41 -Goal
    3.42 -    "!!X. [| mono(f);  a: X;  X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
    3.43 +Goal "[| mono(f);  a: X;  X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
    3.44  by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
    3.45  by (REPEAT (ares_tac [UnI1, Un_least] 1));
    3.46  qed "coinduct";
    3.47 @@ -129,16 +126,6 @@
    3.48  qed "def_coinduct3";
    3.49  
    3.50  (*Monotonicity of gfp!*)
    3.51 -val prems = goal Gfp.thy
    3.52 -    "[| mono(f);  !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
    3.53 -by (rtac gfp_upperbound 1);
    3.54 -by (rtac subset_trans 1);
    3.55 -by (rtac gfp_lemma2 1);
    3.56 -by (resolve_tac prems 1);
    3.57 -by (resolve_tac prems 1);
    3.58 -val gfp_mono = result();
    3.59 -
    3.60 -(*Monotonicity of gfp!*)
    3.61  val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
    3.62  by (rtac (gfp_upperbound RS gfp_least) 1);
    3.63  by (etac (prem RSN (2,subset_trans)) 1);
     4.1 --- a/src/HOL/IOA/IOA.ML	Wed Jul 15 14:13:18 1998 +0200
     4.2 +++ b/src/HOL/IOA/IOA.ML	Wed Jul 15 14:19:02 1998 +0200
     4.3 @@ -20,7 +20,7 @@
     4.4    qed "ioa_triple_proj";
     4.5  
     4.6  Goalw [ioa_def,state_trans_def,actions_def, is_asig_def]
     4.7 -  "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
     4.8 +  "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
     4.9    by (REPEAT(etac conjE 1));
    4.10    by (EVERY1[etac allE, etac impE, atac]);
    4.11    by (Asm_full_simp_tac 1);
    4.12 @@ -118,7 +118,7 @@
    4.13  
    4.14  (* Every state in an execution is reachable *)
    4.15  Goalw [reachable_def] 
    4.16 -"!!A. ex:executions(A) ==> !n. reachable A (snd ex n)";
    4.17 +"ex:executions(A) ==> !n. reachable A (snd ex n)";
    4.18    by (Fast_tac 1);
    4.19  qed "states_of_exec_reachable";
    4.20  
    4.21 @@ -161,13 +161,13 @@
    4.22  qed"externals_of_par"; 
    4.23  
    4.24  Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
    4.25 - "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    4.26 + "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    4.27  by (Asm_full_simp_tac 1);
    4.28  by (best_tac (claset() addEs [equalityCE]) 1);
    4.29  qed"ext1_is_not_int2";
    4.30  
    4.31  Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
    4.32 - "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    4.33 + "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    4.34  by (Asm_full_simp_tac 1);
    4.35  by (best_tac (claset() addEs [equalityCE]) 1);
    4.36  qed"ext2_is_not_int1";
     5.1 --- a/src/HOL/Induct/Comb.ML	Wed Jul 15 14:13:18 1998 +0200
     5.2 +++ b/src/HOL/Induct/Comb.ML	Wed Jul 15 14:19:02 1998 +0200
     5.3 @@ -25,7 +25,7 @@
     5.4  
     5.5  (*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
     5.6  Goalw [diamond_def]
     5.7 -    "!!r. [| diamond(r);  (x,y):r^* |] ==> \ 
     5.8 +    "[| diamond(r);  (x,y):r^* |] ==> \ 
     5.9  \         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
    5.10  by (etac rtrancl_induct 1);
    5.11  by (Blast_tac 1);
    5.12 @@ -118,8 +118,7 @@
    5.13  qed "S1_parcontractD";
    5.14  AddSDs [S1_parcontractD];
    5.15  
    5.16 -Goal
    5.17 - "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
    5.18 +Goal "S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
    5.19  by (Blast_tac 1);
    5.20  qed "S2_parcontractD";
    5.21  AddSDs [S2_parcontractD];
     6.1 --- a/src/HOL/Induct/Exp.ML	Wed Jul 15 14:13:18 1998 +0200
     6.2 +++ b/src/HOL/Induct/Exp.ML	Wed Jul 15 14:19:02 1998 +0200
     6.3 @@ -67,9 +67,8 @@
     6.4    the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
     6.5    functional on the argument (c,s).
     6.6  *)
     6.7 -Goal
     6.8 -    "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
     6.9 -\         ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
    6.10 +Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
    6.11 +\     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
    6.12  by (etac exec.induct 1);
    6.13  by (ALLGOALS Full_simp_tac);
    6.14  by (Blast_tac 3);
     7.1 --- a/src/HOL/Induct/LList.ML	Wed Jul 15 14:13:18 1998 +0200
     7.2 +++ b/src/HOL/Induct/LList.ML	Wed Jul 15 14:19:02 1998 +0200
     7.3 @@ -32,7 +32,7 @@
     7.4  ***)
     7.5  
     7.6  Goalw [list_Fun_def]
     7.7 -    "!!M. [| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
     7.8 +    "[| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
     7.9  by (etac llist.coinduct 1);
    7.10  by (etac (subsetD RS CollectD) 1);
    7.11  by (assume_tac 1);
    7.12 @@ -44,7 +44,7 @@
    7.13  AddIffs [list_Fun_NIL_I];
    7.14  
    7.15  Goalw [list_Fun_def,CONS_def]
    7.16 -    "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
    7.17 +    "[| M: A;  N: X |] ==> CONS M N : list_Fun A X";
    7.18  by (Fast_tac 1);
    7.19  qed "list_Fun_CONS_I";
    7.20  Addsimps [list_Fun_CONS_I];
    7.21 @@ -52,7 +52,7 @@
    7.22  
    7.23  (*Utilise the "strong" part, i.e. gfp(f)*)
    7.24  Goalw (llist.defs @ [list_Fun_def])
    7.25 -    "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))";
    7.26 +    "M: llist(A) ==> M : list_Fun A (X Un llist(A))";
    7.27  by (etac (llist.mono RS gfp_fun_UnI2) 1);
    7.28  qed "list_Fun_llist_I";
    7.29  
    7.30 @@ -195,7 +195,7 @@
    7.31  qed "LListD_Fun_mono";
    7.32  
    7.33  Goalw [LListD_Fun_def]
    7.34 -    "!!M. [| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
    7.35 +    "[| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
    7.36  by (etac LListD.coinduct 1);
    7.37  by (etac (subsetD RS CollectD) 1);
    7.38  by (assume_tac 1);
    7.39 @@ -206,13 +206,13 @@
    7.40  qed "LListD_Fun_NIL_I";
    7.41  
    7.42  Goalw [LListD_Fun_def,CONS_def]
    7.43 - "!!x. [| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
    7.44 + "[| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
    7.45  by (Fast_tac 1);
    7.46  qed "LListD_Fun_CONS_I";
    7.47  
    7.48  (*Utilise the "strong" part, i.e. gfp(f)*)
    7.49  Goalw (LListD.defs @ [LListD_Fun_def])
    7.50 -    "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
    7.51 +    "M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
    7.52  by (etac (LListD.mono RS gfp_fun_UnI2) 1);
    7.53  qed "LListD_Fun_LListD_I";
    7.54  
    7.55 @@ -236,7 +236,7 @@
    7.56  qed "LListD_eq_diag";
    7.57  
    7.58  Goal 
    7.59 -    "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
    7.60 +    "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
    7.61  by (rtac (LListD_eq_diag RS subst) 1);
    7.62  by (rtac LListD_Fun_LListD_I 1);
    7.63  by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
    7.64 @@ -247,7 +247,7 @@
    7.65        [also admits true equality]
    7.66     Replace "A" by some particular set, like {x.True}??? *)
    7.67  Goal 
    7.68 -    "!!r. [| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
    7.69 +    "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
    7.70  \         |] ==>  M=N";
    7.71  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
    7.72  by (etac LListD_coinduct 1);
    7.73 @@ -539,7 +539,7 @@
    7.74  
    7.75  (*weak co-induction: bisimulation and case analysis on both variables*)
    7.76  Goal
    7.77 -    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    7.78 +    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    7.79  by (res_inst_tac
    7.80      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
    7.81  by (Fast_tac 1);
    7.82 @@ -552,7 +552,7 @@
    7.83  
    7.84  (*strong co-induction: bisimulation and case analysis on one variable*)
    7.85  Goal
    7.86 -    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    7.87 +    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    7.88  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
    7.89  by (etac imageI 1);
    7.90  by (rtac image_subsetI 1);
    7.91 @@ -620,7 +620,7 @@
    7.92  (*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
    7.93  
    7.94  Goalw [LListD_Fun_def]
    7.95 -    "!!r A. r <= (llist A) Times (llist A) ==> \
    7.96 +    "r <= (llist A) Times (llist A) ==> \
    7.97  \           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
    7.98  by (stac llist_unfold 1);
    7.99  by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
   7.100 @@ -654,7 +654,7 @@
   7.101  
   7.102  (*Surprisingly hard to prove.  Used with lfilter*)
   7.103  Goalw [llistD_Fun_def, prod_fun_def]
   7.104 -    "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
   7.105 +    "A<=B ==> llistD_Fun A <= llistD_Fun B";
   7.106  by Auto_tac;
   7.107  by (rtac image_eqI 1);
   7.108  by (fast_tac (claset() addss (simpset())) 1);
   7.109 @@ -693,7 +693,7 @@
   7.110  
   7.111  (*Utilise the "strong" part, i.e. gfp(f)*)
   7.112  Goalw [llistD_Fun_def]
   7.113 -     "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   7.114 +     "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   7.115  by (rtac (Rep_llist_inverse RS subst) 1);
   7.116  by (rtac prod_fun_imageI 1);
   7.117  by (stac image_Un 1);
     8.1 --- a/src/HOL/Induct/SList.ML	Wed Jul 15 14:13:18 1998 +0200
     8.2 +++ b/src/HOL/Induct/SList.ML	Wed Jul 15 14:19:02 1998 +0200
     8.3 @@ -165,12 +165,12 @@
     8.4  (** pred_sexp lemmas **)
     8.5  
     8.6  Goalw [CONS_def,In1_def]
     8.7 -    "!!M. [| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
     8.8 +    "[| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
     8.9  by (Asm_simp_tac 1);
    8.10  qed "pred_sexp_CONS_I1";
    8.11  
    8.12  Goalw [CONS_def,In1_def]
    8.13 -    "!!M. [| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
    8.14 +    "[| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
    8.15  by (Asm_simp_tac 1);
    8.16  qed "pred_sexp_CONS_I2";
    8.17  
     9.1 --- a/src/HOL/Induct/Simult.ML	Wed Jul 15 14:13:18 1998 +0200
     9.2 +++ b/src/HOL/Induct/Simult.ML	Wed Jul 15 14:19:02 1998 +0200
     9.3 @@ -56,7 +56,7 @@
     9.4  
     9.5  (*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
     9.6  Goalw [Part_def]
     9.7 - "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
     9.8 + "! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
     9.9  \                   (M: Part (TF A) In1 --> Q(M)) \
    9.10  \  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
    9.11  by (Blast_tac 1);
    9.12 @@ -135,7 +135,7 @@
    9.13  AddSEs [Scons_inject];
    9.14  
    9.15  Goalw TF_Rep_defs
    9.16 -    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
    9.17 +    "[| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
    9.18  by (Blast_tac 1);
    9.19  qed "TCONS_I";
    9.20  
    9.21 @@ -145,7 +145,7 @@
    9.22  qed "FNIL_I";
    9.23  
    9.24  Goalw TF_Rep_defs
    9.25 -    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
    9.26 +    "[| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
    9.27  \         FCONS M N : Part (TF A) In1";
    9.28  by (Blast_tac 1);
    9.29  qed "FCONS_I";
    9.30 @@ -244,7 +244,7 @@
    9.31  (** conversion rules for TF_rec **)
    9.32  
    9.33  Goalw [TCONS_def]
    9.34 -    "!!M N. [| M: sexp;  N: sexp |] ==>         \
    9.35 +    "[| M: sexp;  N: sexp |] ==>         \
    9.36  \           TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
    9.37  by (rtac (TF_rec_unfold RS trans) 1);
    9.38  by (simp_tac (simpset() addsimps [Case_In0, Split]) 1);
    9.39 @@ -257,7 +257,7 @@
    9.40  qed "TF_rec_FNIL";
    9.41  
    9.42  Goalw [FCONS_def]
    9.43 - "!!M N. [| M: sexp;  N: sexp |] ==>    \
    9.44 + "[| M: sexp;  N: sexp |] ==>    \
    9.45  \        TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
    9.46  by (rtac (TF_rec_unfold RS trans) 1);
    9.47  by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
    10.1 --- a/src/HOL/Integ/Equiv.ML	Wed Jul 15 14:13:18 1998 +0200
    10.2 +++ b/src/HOL/Integ/Equiv.ML	Wed Jul 15 14:19:02 1998 +0200
    10.3 @@ -17,17 +17,17 @@
    10.4  (** first half: equiv A r ==> r^-1 O r = r **)
    10.5  
    10.6  Goalw [trans_def,sym_def,converse_def]
    10.7 -    "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
    10.8 +    "[| sym(r); trans(r) |] ==> r^-1 O r <= r";
    10.9  by (Blast_tac 1);
   10.10  qed "sym_trans_comp_subset";
   10.11  
   10.12  Goalw [refl_def]
   10.13 -    "!!A r. refl A r ==> r <= r^-1 O r";
   10.14 +    "refl A r ==> r <= r^-1 O r";
   10.15  by (Blast_tac 1);
   10.16  qed "refl_comp_subset";
   10.17  
   10.18  Goalw [equiv_def]
   10.19 -    "!!A r. equiv A r ==> r^-1 O r = r";
   10.20 +    "equiv A r ==> r^-1 O r = r";
   10.21  by (Clarify_tac 1);
   10.22  by (rtac equalityI 1);
   10.23  by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1));
   10.24 @@ -35,7 +35,7 @@
   10.25  
   10.26  (*second half*)
   10.27  Goalw [equiv_def,refl_def,sym_def,trans_def]
   10.28 -    "!!A r. [| r^-1 O r = r;  Domain(r) = A |] ==> equiv A r";
   10.29 +    "[| r^-1 O r = r;  Domain(r) = A |] ==> equiv A r";
   10.30  by (etac equalityE 1);
   10.31  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
   10.32  by (ALLGOALS Fast_tac);
   10.33 @@ -45,7 +45,7 @@
   10.34  
   10.35  (*Lemma for the next result*)
   10.36  Goalw [equiv_def,trans_def,sym_def]
   10.37 -    "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
   10.38 +    "[| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
   10.39  by (Blast_tac 1);
   10.40  qed "equiv_class_subset";
   10.41  
   10.42 @@ -56,24 +56,24 @@
   10.43  qed "equiv_class_eq";
   10.44  
   10.45  Goalw [equiv_def,refl_def]
   10.46 -    "!!A r. [| equiv A r;  a: A |] ==> a: r^^{a}";
   10.47 +    "[| equiv A r;  a: A |] ==> a: r^^{a}";
   10.48  by (Blast_tac 1);
   10.49  qed "equiv_class_self";
   10.50  
   10.51  (*Lemma for the next result*)
   10.52  Goalw [equiv_def,refl_def]
   10.53 -    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
   10.54 +    "[| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
   10.55  by (Blast_tac 1);
   10.56  qed "subset_equiv_class";
   10.57  
   10.58  Goal
   10.59 -    "!!A r. [| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
   10.60 +    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
   10.61  by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
   10.62  qed "eq_equiv_class";
   10.63  
   10.64  (*thus r^^{a} = r^^{b} as well*)
   10.65  Goalw [equiv_def,trans_def,sym_def]
   10.66 -    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
   10.67 +    "[| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
   10.68  by (Blast_tac 1);
   10.69  qed "equiv_class_nondisjoint";
   10.70  
   10.71 @@ -83,13 +83,13 @@
   10.72  qed "equiv_type";
   10.73  
   10.74  Goal
   10.75 -    "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   10.76 +    "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   10.77  by (blast_tac (claset() addSIs [equiv_class_eq]
   10.78  	               addDs [eq_equiv_class, equiv_type]) 1);
   10.79  qed "equiv_class_eq_iff";
   10.80  
   10.81  Goal
   10.82 -    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   10.83 +    "[| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   10.84  by (blast_tac (claset() addSIs [equiv_class_eq]
   10.85  	               addDs [eq_equiv_class, equiv_type]) 1);
   10.86  qed "eq_equiv_class_iff";
   10.87 @@ -112,12 +112,12 @@
   10.88  qed "quotientE";
   10.89  
   10.90  Goalw [equiv_def,refl_def,quotient_def]
   10.91 -    "!!A r. equiv A r ==> Union(A/r) = A";
   10.92 +    "equiv A r ==> Union(A/r) = A";
   10.93  by (blast_tac (claset() addSIs [equalityI]) 1);
   10.94  qed "Union_quotient";
   10.95  
   10.96  Goalw [quotient_def]
   10.97 -    "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y = {})";
   10.98 +    "[| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y = {})";
   10.99  by (safe_tac (claset() addSIs [equiv_class_eq]));
  10.100  by (assume_tac 1);
  10.101  by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
  10.102 @@ -178,12 +178,12 @@
  10.103  
  10.104  
  10.105  Goalw [congruent_def,congruent2_def,equiv_def,refl_def]
  10.106 -    "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
  10.107 +    "[| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
  10.108  by (Blast_tac 1);
  10.109  qed "congruent2_implies_congruent";
  10.110  
  10.111  Goalw [congruent_def]
  10.112 -    "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> \
  10.113 +    "[| equiv A r;  congruent2 r b;  a: A |] ==> \
  10.114  \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
  10.115  by (Clarify_tac 1);
  10.116  by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
  10.117 @@ -194,7 +194,7 @@
  10.118  qed "congruent2_implies_congruent_UN";
  10.119  
  10.120  Goal
  10.121 -    "!!A r. [| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
  10.122 +    "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
  10.123  \    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
  10.124  by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
  10.125                                       congruent2_implies_congruent,
  10.126 @@ -252,7 +252,7 @@
  10.127  qed "finite_quotient";
  10.128  
  10.129  Goalw [quotient_def]
  10.130 -    "!!A. [| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
  10.131 +    "[| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
  10.132  by (rtac finite_subset 1);
  10.133  by (assume_tac 2);
  10.134  by (Blast_tac 1);
    11.1 --- a/src/HOL/Integ/Integ.ML	Wed Jul 15 14:13:18 1998 +0200
    11.2 +++ b/src/HOL/Integ/Integ.ML	Wed Jul 15 14:19:02 1998 +0200
    11.3 @@ -551,7 +551,7 @@
    11.4  (* Theorems about less and less_equal *)
    11.5  
    11.6  Goalw [zless_def, znegative_def, zdiff_def, znat_def] 
    11.7 -    "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
    11.8 +    "w<z ==> ? n. z = w + $#(Suc(n))";
    11.9  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   11.10  by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   11.11  by Safe_tac;
    12.1 --- a/src/HOL/NatDef.ML	Wed Jul 15 14:13:18 1998 +0200
    12.2 +++ b/src/HOL/NatDef.ML	Wed Jul 15 14:19:02 1998 +0200
    12.3 @@ -519,8 +519,7 @@
    12.4  qed "Suc_leD";
    12.5  
    12.6  (* stronger version of Suc_leD *)
    12.7 -Goalw [le_def] 
    12.8 -        "!!m. Suc m <= n ==> m < n";
    12.9 +Goalw [le_def] "Suc m <= n ==> m < n";
   12.10  by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   12.11  by (cut_facts_tac [less_linear] 1);
   12.12  by (Blast_tac 1);
    13.1 --- a/src/HOL/Real/Lubs.ML	Wed Jul 15 14:13:18 1998 +0200
    13.2 +++ b/src/HOL/Real/Lubs.ML	Wed Jul 15 14:19:02 1998 +0200
    13.3 @@ -42,12 +42,12 @@
    13.4  qed "leastPD3";
    13.5  
    13.6  Goalw [isLub_def,isUb_def,leastP_def] 
    13.7 -      "!!x. isLub R S x ==> S *<= x";
    13.8 +      "isLub R S x ==> S *<= x";
    13.9  by (Step_tac 1);
   13.10  qed "isLubD1";
   13.11  
   13.12  Goalw [isLub_def,isUb_def,leastP_def] 
   13.13 -      "!!x. isLub R S x ==> x: R";
   13.14 +      "isLub R S x ==> x: R";
   13.15  by (Step_tac 1);
   13.16  qed "isLubD1a";
   13.17  
   13.18 @@ -68,7 +68,7 @@
   13.19  qed "isLubI1";
   13.20  
   13.21  Goalw [isLub_def,leastP_def] 
   13.22 -      "!!x. [| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x";
   13.23 +      "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x";
   13.24  by (Step_tac 1);
   13.25  qed "isLubI2";
   13.26  
    14.1 --- a/src/HOL/Real/PNat.ML	Wed Jul 15 14:13:18 1998 +0200
    14.2 +++ b/src/HOL/Real/PNat.ML	Wed Jul 15 14:19:02 1998 +0200
    14.3 @@ -241,7 +241,7 @@
    14.4    (*** pnat_less ***)
    14.5  
    14.6  Goalw [pnat_less_def] 
    14.7 -      "!!x. [| x < (y::pnat); y < z |] ==> x < z";
    14.8 +      "[| x < (y::pnat); y < z |] ==> x < z";
    14.9  by ((etac less_trans 1) THEN assume_tac 1);
   14.10  qed "pnat_less_trans";
   14.11  
   14.12 @@ -259,7 +259,7 @@
   14.13  bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE);
   14.14  
   14.15  Goalw [pnat_less_def] 
   14.16 -     "!!x. x < (y::pnat) ==> x ~= y";
   14.17 +     "x < (y::pnat) ==> x ~= y";
   14.18  by Auto_tac;
   14.19  qed "pnat_less_not_refl2";
   14.20  
   14.21 @@ -279,7 +279,7 @@
   14.22  bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
   14.23  
   14.24  Goalw [pnat_less_def] 
   14.25 -     "!!x. x < (y::pnat) ==> Rep_pnat y ~= 1";
   14.26 +     "x < (y::pnat) ==> Rep_pnat y ~= 1";
   14.27  by (auto_tac (claset(),simpset() 
   14.28      addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
   14.29  qed "Rep_pnat_gt_implies_not0";
   14.30 @@ -526,7 +526,7 @@
   14.31  qed "pnat_add_less_mono";
   14.32  
   14.33  Goalw [pnat_less_def]
   14.34 -     "!!f. [| !!i j::pnat. i<j ==> f(i) < f(j);       \
   14.35 +"!!f. [| !!i j::pnat. i<j ==> f(i) < f(j);       \
   14.36  \        i <= j                                 \
   14.37  \     |] ==> f(i) <= (f(j)::pnat)";
   14.38  by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
    15.1 --- a/src/HOL/Real/PRat.ML	Wed Jul 15 14:13:18 1998 +0200
    15.2 +++ b/src/HOL/Real/PRat.ML	Wed Jul 15 14:19:02 1998 +0200
    15.3 @@ -12,7 +12,7 @@
    15.4  (*** Proving that ratrel is an equivalence relation ***)
    15.5  
    15.6  Goal
    15.7 -    "!! x1. [| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
    15.8 +    "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
    15.9  \            ==> x1 * y3 = x3 * y1";        
   15.10  by (res_inst_tac [("k1","y2")] (pnat_mult_cancel1 RS iffD1) 1);
   15.11  by (auto_tac (claset(), simpset() addsimps [pnat_mult_assoc RS sym]));
   15.12 @@ -30,7 +30,7 @@
   15.13  qed "ratrel_iff";
   15.14  
   15.15  Goalw [ratrel_def]
   15.16 -    "!!x1 x2. [| x1 * y2 = x2 * y1 |] ==> ((x1,y1),(x2,y2)): ratrel";
   15.17 +    "[| x1 * y2 = x2 * y1 |] ==> ((x1,y1),(x2,y2)): ratrel";
   15.18  by (Fast_tac  1);
   15.19  qed "ratrelI";
   15.20  
   15.21 @@ -143,8 +143,7 @@
   15.22  by (simp_tac (simpset() addsimps [qinv]) 1);
   15.23  qed "qinv_1";
   15.24  
   15.25 -Goal 
   15.26 -     "!!(x1::pnat). [| x1 * y2 = x2 * y1 |] ==> \
   15.27 +Goal "!!(x1::pnat). [| x1 * y2 = x2 * y1 |] ==> \
   15.28  \     (x * y1 + x1 * ya) * (ya * y2) = (x * y2 + x2 * ya) * (ya * y1)";
   15.29  by (auto_tac (claset() addSIs [pnat_same_multI2],
   15.30         simpset() addsimps [pnat_add_mult_distrib,
   15.31 @@ -367,17 +366,15 @@
   15.32  by (Fast_tac 1);
   15.33  qed "prat_lessE_lemma";
   15.34  
   15.35 -Goal 
   15.36 -     "!! Q1. [| Q1 < (Q2::prat); \
   15.37 -\        !! (Q3::prat). Q1 + Q3 = Q2 ==> P |] \
   15.38 -\     ==> P";
   15.39 +Goal "!!P. [| Q1 < (Q2::prat); \
   15.40 +\             !! (Q3::prat). Q1 + Q3 = Q2 ==> P |] \
   15.41 +\          ==> P";
   15.42  by (dtac (prat_lessE_lemma RS mp) 1);
   15.43  by Auto_tac;
   15.44  qed "prat_lessE";
   15.45  
   15.46  (* qless is a strong order i.e nonreflexive and transitive *)
   15.47 -Goal 
   15.48 -     "!!(q1::prat). [| q1 < q2; q2 < q3 |] ==> q1 < q3";
   15.49 +Goal "!!(q1::prat). [| q1 < q2; q2 < q3 |] ==> q1 < q3";
   15.50  by (REPEAT(dtac (prat_lessE_lemma RS mp) 1));
   15.51  by (REPEAT(etac exE 1));
   15.52  by (hyp_subst_tac 1);
   15.53 @@ -653,14 +650,14 @@
   15.54  qed "not_less_not_eq_prat_less";
   15.55  
   15.56  Goalw [prat_less_def] 
   15.57 -      "!!x. [| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::prat)";
   15.58 +      "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::prat)";
   15.59  by (REPEAT(etac exE 1));
   15.60  by (res_inst_tac [("x","T+Ta")] exI 1);
   15.61  by (auto_tac (claset(),simpset() addsimps prat_add_ac));
   15.62  qed "prat_add_less_mono";
   15.63  
   15.64  Goalw [prat_less_def] 
   15.65 -      "!!x. [| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::prat)";
   15.66 +      "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::prat)";
   15.67  by (REPEAT(etac exE 1));
   15.68  by (res_inst_tac [("x","T*Ta+T*x2+x1*Ta")] exI 1);
   15.69  by (auto_tac (claset(),simpset() addsimps prat_add_ac @ 
    16.1 --- a/src/HOL/Real/PReal.ML	Wed Jul 15 14:13:18 1998 +0200
    16.2 +++ b/src/HOL/Real/PReal.ML	Wed Jul 15 14:19:02 1998 +0200
    16.3 @@ -50,21 +50,21 @@
    16.4  qed "mem_Rep_preal_Ex";
    16.5  
    16.6  Goalw [preal_def] 
    16.7 -      "!!A. [| {} < A; A < {q::prat. True}; \
    16.8 +      "[| {} < A; A < {q::prat. True}; \
    16.9  \              (!y: A. ((!z. z < y --> z: A) & \
   16.10  \                        (? u: A. y < u))) |] ==> A : preal";
   16.11  by (Fast_tac 1);
   16.12  qed "prealI1";
   16.13      
   16.14  Goalw [preal_def] 
   16.15 -      "!!A. [| {} < A; A < {q::prat. True}; \
   16.16 +      "[| {} < A; A < {q::prat. True}; \
   16.17  \              !y: A. (!z. z < y --> z: A); \
   16.18  \              !y: A. (? u: A. y < u) |] ==> A : preal";
   16.19  by (Best_tac 1);
   16.20  qed "prealI2";
   16.21  
   16.22  Goalw [preal_def] 
   16.23 -      "!!A. A : preal ==> {} < A & A < {q::prat. True} & \
   16.24 +      "A : preal ==> {} < A & A < {q::prat. True} & \
   16.25  \                         (!y: A. ((!z. z < y --> z: A) & \
   16.26  \                                  (? u: A. y < u)))";
   16.27  by (Fast_tac 1);
   16.28 @@ -76,38 +76,31 @@
   16.29  Addsimps [Abs_preal_inverse];
   16.30  
   16.31  
   16.32 -Goalw [preal_def] 
   16.33 -      "!!A. A : preal ==> {} < A";
   16.34 +Goalw [preal_def] "A : preal ==> {} < A";
   16.35  by (Fast_tac 1);
   16.36  qed "prealE_lemma1";
   16.37  
   16.38 -Goalw [preal_def] 
   16.39 -      "!!A. A : preal ==> A < {q::prat. True}";
   16.40 +Goalw [preal_def] "A : preal ==> A < {q::prat. True}";
   16.41  by (Fast_tac 1);
   16.42  qed "prealE_lemma2";
   16.43  
   16.44 -Goalw [preal_def] 
   16.45 -      "!!A. A : preal ==> !y: A. (!z. z < y --> z: A)";
   16.46 +Goalw [preal_def] "A : preal ==> !y: A. (!z. z < y --> z: A)";
   16.47  by (Fast_tac 1);
   16.48  qed "prealE_lemma3";
   16.49  
   16.50 -Goal 
   16.51 -      "!!A. [| A : preal; y: A |] ==> (!z. z < y --> z: A)";
   16.52 +Goal "[| A : preal; y: A |] ==> (!z. z < y --> z: A)";
   16.53  by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
   16.54  qed "prealE_lemma3a";
   16.55  
   16.56 -Goal 
   16.57 -      "!!A. [| A : preal; y: A; z < y |] ==> z: A";
   16.58 +Goal "[| A : preal; y: A; z < y |] ==> z: A";
   16.59  by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
   16.60  qed "prealE_lemma3b";
   16.61  
   16.62 -Goalw [preal_def] 
   16.63 -      "!!A. A : preal ==> !y: A. (? u: A. y < u)";
   16.64 +Goalw [preal_def] "A : preal ==> !y: A. (? u: A. y < u)";
   16.65  by (Fast_tac 1);
   16.66  qed "prealE_lemma4";
   16.67  
   16.68 -Goal 
   16.69 -      "!!A. [| A : preal; y: A |] ==> ? u: A. y < u";
   16.70 +Goal "[| A : preal; y: A |] ==> ? u: A. y < u";
   16.71  by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
   16.72  qed "prealE_lemma4a";
   16.73  
   16.74 @@ -177,10 +170,9 @@
   16.75  by (Fast_tac  1);
   16.76  qed "preal_lessE_lemma";
   16.77  
   16.78 -Goal 
   16.79 -     "!! R1. [| R1 < (R2::preal); \
   16.80 -\               (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \
   16.81 -\     ==> P";
   16.82 +Goal "!!P. [| R1 < (R2::preal); \
   16.83 +\             (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \
   16.84 +\          ==> P";
   16.85  by (dtac (preal_lessE_lemma RS mp) 1);
   16.86  by Auto_tac;
   16.87  qed "preal_lessE";
   16.88 @@ -445,14 +437,14 @@
   16.89  
   16.90   (** lemmas **)
   16.91  Goalw [preal_add_def] 
   16.92 -      "!!R. z: Rep_preal(R+S) ==> \
   16.93 +      "z: Rep_preal(R+S) ==> \
   16.94  \           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
   16.95  by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
   16.96  by (Fast_tac 1);
   16.97  qed "mem_Rep_preal_addD";
   16.98  
   16.99  Goalw [preal_add_def] 
  16.100 -      "!!R. ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
  16.101 +      "? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
  16.102  \      ==> z: Rep_preal(R+S)";
  16.103  by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
  16.104  by (Fast_tac 1);
  16.105 @@ -464,14 +456,14 @@
  16.106  qed "mem_Rep_preal_add_iff";
  16.107  
  16.108  Goalw [preal_mult_def] 
  16.109 -      "!!R. z: Rep_preal(R*S) ==> \
  16.110 +      "z: Rep_preal(R*S) ==> \
  16.111  \           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
  16.112  by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
  16.113  by (Fast_tac 1);
  16.114  qed "mem_Rep_preal_multD";
  16.115  
  16.116  Goalw [preal_mult_def] 
  16.117 -      "!!R. ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
  16.118 +      "? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
  16.119  \      ==> z: Rep_preal(R*S)";
  16.120  by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
  16.121  by (Fast_tac 1);
  16.122 @@ -774,14 +766,14 @@
  16.123  (*** Properties of <= ***)
  16.124  
  16.125  Goalw [preal_le_def,psubset_def,preal_less_def] 
  16.126 -                     "!!w. z<=w ==> ~(w<(z::preal))";
  16.127 +                     "z<=w ==> ~(w<(z::preal))";
  16.128  by (auto_tac  (claset() addDs [equalityI],simpset()));
  16.129  qed "preal_leD";
  16.130  
  16.131  val preal_leE = make_elim preal_leD;
  16.132  
  16.133  Goalw [preal_le_def,psubset_def,preal_less_def]
  16.134 -                   "!!z. ~ z <= w ==> w<(z::preal)";
  16.135 +                   "~ z <= w ==> w<(z::preal)";
  16.136  by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
  16.137  by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));
  16.138  qed "not_preal_leE";
  16.139 @@ -795,7 +787,7 @@
  16.140  qed "preal_less_le_iff";
  16.141  
  16.142  Goalw [preal_le_def,preal_less_def,psubset_def] 
  16.143 -                  "!!z. z < w ==> z <= (w::preal)";
  16.144 +                  "z < w ==> z <= (w::preal)";
  16.145  by (Fast_tac 1);
  16.146  qed "preal_less_imp_le";
  16.147  
  16.148 @@ -878,7 +870,7 @@
  16.149  
  16.150  (** Part 1 of Dedekind sections def **)
  16.151  Goalw [preal_less_def]
  16.152 -     "!!A. A < B ==> \
  16.153 +     "A < B ==> \
  16.154  \     ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  16.155  by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
  16.156  by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
  16.157 @@ -886,7 +878,7 @@
  16.158  qed "lemma_ex_mem_less_left_add1";
  16.159  
  16.160  Goal
  16.161 -     "!!A. A < B ==> \
  16.162 +     "A < B ==> \
  16.163  \       {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
  16.164  by (dtac lemma_ex_mem_less_left_add1 1);
  16.165  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
  16.166 @@ -1074,16 +1066,14 @@
  16.167  
  16.168  Addsimps [preal_add_less_iff2];
  16.169  
  16.170 -Goal 
  16.171 -      "!!x1. [| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
  16.172 +Goal "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
  16.173  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  16.174      simpset() addsimps  preal_add_ac));
  16.175  by (rtac (preal_add_assoc RS subst) 1);
  16.176  by (rtac preal_self_less_add_right 1);
  16.177  qed "preal_add_less_mono";
  16.178  
  16.179 -Goal 
  16.180 -      "!!x1. [| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
  16.181 +Goal "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
  16.182  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  16.183                simpset() addsimps [preal_add_mult_distrib,
  16.184                preal_add_mult_distrib2,preal_self_less_add_left,
    17.1 --- a/src/HOL/Real/Real.ML	Wed Jul 15 14:13:18 1998 +0200
    17.2 +++ b/src/HOL/Real/Real.ML	Wed Jul 15 14:19:02 1998 +0200
    17.3 @@ -8,8 +8,7 @@
    17.4  
    17.5  (*** Proving that realrel is an equivalence relation ***)
    17.6  
    17.7 -Goal
    17.8 -    "!! x1. [| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
    17.9 +Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
   17.10  \            ==> x1 + y3 = x3 + y1";        
   17.11  by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
   17.12  by (rotate_tac 1 1 THEN dtac sym 1);
   17.13 @@ -27,7 +26,7 @@
   17.14  qed "realrel_iff";
   17.15  
   17.16  Goalw [realrel_def]
   17.17 -    "!!x1 x2. [| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
   17.18 +    "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
   17.19  by (Fast_tac  1);
   17.20  qed "realrelI";
   17.21  
   17.22 @@ -504,13 +503,13 @@
   17.23  qed "real_less_iff";
   17.24  
   17.25  Goalw [real_less_def]
   17.26 - "!!P. [| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \
   17.27 + "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \
   17.28  \         (x2,y2):Rep_real(Q) |] ==> P < (Q::real)";
   17.29  by (Fast_tac 1);
   17.30  qed "real_lessI";
   17.31  
   17.32  Goalw [real_less_def]
   17.33 -     "!! R1. [| R1 < (R2::real); \
   17.34 + "!!P. [| R1 < (R2::real); \
   17.35  \         !!x1 x2 y1 y2. x1 + y2 < x2 + y1 ==> P; \
   17.36  \         !!x1 y1. (x1,y1::preal):Rep_real(R1) ==> P; \ 
   17.37  \         !!x2 y2. (x2,y2::preal):Rep_real(R2) ==> P |] \
   17.38 @@ -519,7 +518,7 @@
   17.39  qed "real_lessE";
   17.40  
   17.41  Goalw [real_less_def]
   17.42 - "!!R1. R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
   17.43 + "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
   17.44  \                                  (x1,y1::preal):Rep_real(R1) & \
   17.45  \                                  (x2,y2):Rep_real(R2))";
   17.46  by (Fast_tac 1);
   17.47 @@ -636,7 +635,7 @@
   17.48  by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   17.49  qed "real_preal_trichotomy";
   17.50  
   17.51 -Goal "!!x. [| !!m. x = %#m ==> P; \
   17.52 +Goal "!!P. [| !!m. x = %#m ==> P; \
   17.53  \             x = 0r ==> P; \
   17.54  \             !!m. x = %~(%#m) ==> P |] ==> P";
   17.55  by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
   17.56 @@ -781,9 +780,8 @@
   17.57                 real_preal_zero_less,real_preal_minus_less_all]));
   17.58  qed "real_linear";
   17.59  
   17.60 -Goal
   17.61 -    "!!(R1::real). [| R1 < R2 ==> P;  R1 = R2 ==> P; \
   17.62 -\          R2 < R1 ==> P |] ==> P";
   17.63 +Goal "!!(R1::real). [| R1 < R2 ==> P;  R1 = R2 ==> P; \
   17.64 +\                      R2 < R1 ==> P |] ==> P";
   17.65  by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
   17.66  by Auto_tac;
   17.67  qed "real_linear_less2";
   17.68 @@ -1172,7 +1170,7 @@
   17.69  qed "real_le_add_order";
   17.70  
   17.71  Goal 
   17.72 -      "!!x. [| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
   17.73 +      "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
   17.74  by (dtac (real_less_iffdef RS iffD2) 1);
   17.75  by (dtac (real_less_iffdef RS iffD2) 1);
   17.76  by (rtac (real_less_iffdef RS iffD1) 1);
   17.77 @@ -1456,8 +1454,7 @@
   17.78  (*------------------------------------------------------------------
   17.79       lemmas about upper bounds and least upper bound
   17.80   ------------------------------------------------------------------*)
   17.81 -Goalw [real_ub_def] 
   17.82 -          "!!S. [| real_ub u S; x : S |] ==> x <= u";
   17.83 +Goalw [real_ub_def] "[| real_ub u S; x : S |] ==> x <= u";
   17.84  by Auto_tac;
   17.85  qed "real_ubD";
   17.86  
    18.1 --- a/src/HOL/Relation.ML	Wed Jul 15 14:13:18 1998 +0200
    18.2 +++ b/src/HOL/Relation.ML	Wed Jul 15 14:19:02 1998 +0200
    18.3 @@ -29,7 +29,7 @@
    18.4  (** Composition of two relations **)
    18.5  
    18.6  Goalw [comp_def]
    18.7 -    "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    18.8 +    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    18.9  by (Blast_tac 1);
   18.10  qed "compI";
   18.11  
   18.12 @@ -72,8 +72,7 @@
   18.13  by (Blast_tac 1);
   18.14  qed "comp_mono";
   18.15  
   18.16 -Goal
   18.17 -    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
   18.18 +Goal "[| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
   18.19  by (Blast_tac 1);
   18.20  qed "comp_subset_Sigma";
   18.21  
   18.22 @@ -84,8 +83,7 @@
   18.23  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
   18.24  qed "transI";
   18.25  
   18.26 -Goalw [trans_def]
   18.27 -    "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
   18.28 +Goalw [trans_def] "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
   18.29  by (Blast_tac 1);
   18.30  qed "transD";
   18.31  
    19.1 --- a/src/HOL/Set.ML	Wed Jul 15 14:13:18 1998 +0200
    19.2 +++ b/src/HOL/Set.ML	Wed Jul 15 14:19:02 1998 +0200
    19.3 @@ -681,8 +681,7 @@
    19.4  by (Blast_tac 1);
    19.5  qed "psubsetI";
    19.6  
    19.7 -Goalw [psubset_def]
    19.8 -    "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    19.9 +Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
   19.10  by Auto_tac;
   19.11  qed "psubset_insertD";
   19.12  
    20.1 --- a/src/HOL/Sum.ML	Wed Jul 15 14:13:18 1998 +0200
    20.2 +++ b/src/HOL/Sum.ML	Wed Jul 15 14:19:02 1998 +0200
    20.3 @@ -166,8 +166,7 @@
    20.4  
    20.5  (** Rules for the Part primitive **)
    20.6  
    20.7 -Goalw [Part_def]
    20.8 -    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
    20.9 +Goalw [Part_def] "[| a : A;  a=h(b) |] ==> a : Part A h";
   20.10  by (Blast_tac 1);
   20.11  qed "Part_eqI";
   20.12  
    21.1 --- a/src/HOL/Trancl.ML	Wed Jul 15 14:13:18 1998 +0200
    21.2 +++ b/src/HOL/Trancl.ML	Wed Jul 15 14:19:02 1998 +0200
    21.3 @@ -281,7 +281,7 @@
    21.4  bind_thm ("trancl_trans", trans_trancl RS transD);
    21.5  
    21.6  Goalw [trancl_def]
    21.7 -  "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
    21.8 +  "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
    21.9  by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl]) 1);
   21.10  qed "rtrancl_trancl_trancl";
   21.11  
   21.12 @@ -329,8 +329,7 @@
   21.13  by (Blast_tac 1);
   21.14  val lemma = result();
   21.15  
   21.16 -Goalw [trancl_def]
   21.17 -    "!!r. r <= A Times A ==> r^+ <= A Times A";
   21.18 +Goalw [trancl_def] "r <= A Times A ==> r^+ <= A Times A";
   21.19  by (blast_tac (claset() addSDs [lemma]) 1);
   21.20  qed "trancl_subset_Sigma";
   21.21  
    22.1 --- a/src/HOL/Univ.ML	Wed Jul 15 14:13:18 1998 +0200
    22.2 +++ b/src/HOL/Univ.ML	Wed Jul 15 14:19:02 1998 +0200
    22.3 @@ -73,7 +73,7 @@
    22.4  qed "Node_K0_I";
    22.5  
    22.6  Goalw [Node_def,Push_def]
    22.7 -    "!!p. p: Node ==> apfst (Push i) p : Node";
    22.8 +    "p: Node ==> apfst (Push i) p : Node";
    22.9  by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
   22.10  qed "Node_Push_I";
   22.11  
   22.12 @@ -489,7 +489,7 @@
   22.13  (*** Equality for Cartesian Product ***)
   22.14  
   22.15  Goalw [dprod_def]
   22.16 -    "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
   22.17 +    "[| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
   22.18  by (Blast_tac 1);
   22.19  qed "dprodI";
   22.20  
    23.1 --- a/src/HOL/W0/Type.ML	Wed Jul 15 14:13:18 1998 +0200
    23.2 +++ b/src/HOL/W0/Type.ML	Wed Jul 15 14:19:02 1998 +0200
    23.3 @@ -8,7 +8,7 @@
    23.4  
    23.5  (* mgu does not introduce new type variables *)
    23.6  Goalw [new_tv_def] 
    23.7 -      "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
    23.8 +      "[|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
    23.9  \            new_tv n u";
   23.10  by (fast_tac (set_cs addDs [mgu_free]) 1);
   23.11  qed "mgu_new";
   23.12 @@ -56,7 +56,7 @@
   23.13  Addsimps [free_tv_id_subst];
   23.14  
   23.15  Goalw [dom_def,cod_def,UNION_def,Bex_def]
   23.16 -  "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s";
   23.17 +  "[| v : free_tv(s n); v~=n |] ==> v : cod s";
   23.18  by (Simp_tac 1);
   23.19  by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
   23.20  by (assume_tac 2);
   23.21 @@ -190,7 +190,7 @@
   23.22  Addsimps [lessI RS less_imp_le RS new_tv_list_le];
   23.23  
   23.24  Goal
   23.25 -  "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
   23.26 +  "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
   23.27  by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   23.28  by (rtac conjI 1);
   23.29  by (slow_tac (HOL_cs addIs [le_trans]) 1);
   23.30 @@ -203,7 +203,7 @@
   23.31  
   23.32  (* new_tv property remains if a substitution is applied *)
   23.33  Goal
   23.34 -  "!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
   23.35 +  "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
   23.36  by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   23.37  qed "new_tv_subst_var";
   23.38  
   23.39 @@ -233,13 +233,13 @@
   23.40  
   23.41  (* composition of substitutions preserves new_tv proposition *)
   23.42  Goal 
   23.43 -     "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
   23.44 +     "[| new_tv n (s::subst); new_tv n r |] ==> \
   23.45  \           new_tv n (($ r) o s)";
   23.46  by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   23.47  qed "new_tv_subst_comp_1";
   23.48  
   23.49  Goal
   23.50 -     "!! n. [| new_tv n (s::subst); new_tv n r |] ==>  \ 
   23.51 +     "[| new_tv n (s::subst); new_tv n r |] ==>  \ 
   23.52  \     new_tv n (%v.$ r (s v))";
   23.53  by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
   23.54  qed "new_tv_subst_comp_2";
   23.55 @@ -248,7 +248,7 @@
   23.56  
   23.57  (* new type variables do not occur freely in a type structure *)
   23.58  Goalw [new_tv_def] 
   23.59 -      "!!n. new_tv n ts ==> n~:(free_tv ts)";
   23.60 +      "new_tv n ts ==> n~:(free_tv ts)";
   23.61  by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
   23.62  qed "new_tv_not_free_tv";
   23.63  Addsimps [new_tv_not_free_tv];
   23.64 @@ -285,8 +285,7 @@
   23.65  by (fast_tac (HOL_cs addss simpset()) 1);
   23.66  qed_spec_mp "eq_free_eq_subst_te";
   23.67  
   23.68 -Goal
   23.69 -  "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
   23.70 +Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
   23.71  by (list.induct_tac "ts" 1);
   23.72  (* case [] *)
   23.73  by (fast_tac (HOL_cs addss simpset()) 1);
   23.74 @@ -294,8 +293,7 @@
   23.75  by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (simpset())) 1);
   23.76  qed_spec_mp "eq_subst_tel_eq_free";
   23.77  
   23.78 -Goal
   23.79 -  "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
   23.80 +Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
   23.81  by (list.induct_tac "ts" 1); 
   23.82  (* case [] *)
   23.83  by (fast_tac (HOL_cs addss simpset()) 1);
   23.84 @@ -305,29 +303,26 @@
   23.85  
   23.86  (* some useful theorems *)
   23.87  Goalw [free_tv_subst] 
   23.88 -      "!!v. v : cod s ==> v : free_tv s";
   23.89 +      "v : cod s ==> v : free_tv s";
   23.90  by (fast_tac set_cs 1);
   23.91  qed "codD";
   23.92   
   23.93  Goalw [free_tv_subst,dom_def] 
   23.94 -      "!! x. x ~: free_tv s ==> s x = TVar x";
   23.95 +      "x ~: free_tv s ==> s x = TVar x";
   23.96  by (fast_tac set_cs 1);
   23.97  qed "not_free_impl_id";
   23.98  
   23.99 -Goalw [new_tv_def] 
  23.100 -      "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
  23.101 +Goalw [new_tv_def] "[| new_tv n t; m:free_tv t |] ==> m<n";
  23.102  by (fast_tac HOL_cs 1 );
  23.103  qed "free_tv_le_new_tv";
  23.104  
  23.105 -Goal
  23.106 -     "free_tv (s (v::nat)) <= insert v (cod s)";
  23.107 +Goal "free_tv (s (v::nat)) <= insert v (cod s)";
  23.108  by (expand_case_tac "v:dom s" 1);
  23.109  by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
  23.110  by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
  23.111  qed "free_tv_subst_var";
  23.112  
  23.113 -Goal 
  23.114 -     "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
  23.115 +Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
  23.116  by (typ.induct_tac "t" 1);
  23.117  (* case TVar n *)
  23.118  by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
  23.119 @@ -335,8 +330,7 @@
  23.120  by (fast_tac (set_cs addss simpset()) 1);
  23.121  qed "free_tv_app_subst_te";     
  23.122  
  23.123 -Goal 
  23.124 -     "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
  23.125 +Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
  23.126  by (list.induct_tac "ts" 1);
  23.127  (* case [] *)
  23.128  by (Simp_tac 1);
    24.1 --- a/src/HOL/W0/W.ML	Wed Jul 15 14:13:18 1998 +0200
    24.2 +++ b/src/HOL/W0/W.ML	Wed Jul 15 14:19:02 1998 +0200
    24.3 @@ -10,8 +10,7 @@
    24.4  Delsimps (ex_simps @ all_simps);
    24.5  
    24.6  (* correctness of W with respect to has_type *)
    24.7 -Goal
    24.8 -        "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
    24.9 +Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
   24.10  by (expr.induct_tac "e" 1);
   24.11  (* case Var n *)
   24.12  by (Asm_simp_tac 1);
   24.13 @@ -41,8 +40,7 @@
   24.14  
   24.15  
   24.16  (* the resulting type variable is always greater or equal than the given one *)
   24.17 -Goal
   24.18 -        "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
   24.19 +Goal "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
   24.20  by (expr.induct_tac "e" 1);
   24.21  (* case Var(n) *)
   24.22  by (fast_tac (HOL_cs addss simpset()) 1);
   24.23 @@ -72,8 +70,7 @@
   24.24  
   24.25  Addsimps [W_var_ge];
   24.26  
   24.27 -Goal
   24.28 -        "!! s. Ok (s,t,m) = W e a n ==> n<=m";
   24.29 +Goal "Ok (s,t,m) = W e a n ==> n<=m";
   24.30  by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   24.31  qed "W_var_geD";
   24.32  
   24.33 @@ -152,8 +149,7 @@
   24.34  qed_spec_mp "new_tv_W";
   24.35  
   24.36  
   24.37 -Goal
   24.38 -     "!n a s t m v. W e a n = Ok (s,t,m) -->            \
   24.39 +Goal "!n a s t m v. W e a n = Ok (s,t,m) -->            \
   24.40  \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
   24.41  by (expr.induct_tac "e" 1);
   24.42  (* case Var n *)
   24.43 @@ -361,8 +357,7 @@
   24.44  by (Fast_tac 1);
   24.45  qed_spec_mp "W_complete_lemma";
   24.46  
   24.47 -Goal
   24.48 - "!!e. [] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
   24.49 +Goal "[] |- e :: t' ==>  (? s t. (? m. W e [] n = Ok(s,t,m)) &  \
   24.50  \                                 (? r. t' = $r t))";
   24.51  by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
   24.52                  W_complete_lemma 1);
    25.1 --- a/src/HOL/WF.ML	Wed Jul 15 14:13:18 1998 +0200
    25.2 +++ b/src/HOL/WF.ML	Wed Jul 15 14:19:02 1998 +0200
    25.3 @@ -79,7 +79,7 @@
    25.4  val lemma1 = result();
    25.5  
    25.6  Goalw [wf_def]
    25.7 -    "!!r. (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
    25.8 +    "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
    25.9  by (Clarify_tac 1);
   25.10  by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
   25.11  by (Blast_tac 1);
   25.12 @@ -140,7 +140,7 @@
   25.13  "!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]);
   25.14  
   25.15  Goalw [acyclic_def]
   25.16 - "!!r. wf r ==> acyclic r";
   25.17 + "wf r ==> acyclic r";
   25.18  by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
   25.19  qed "wf_acyclic";
   25.20  
   25.21 @@ -171,7 +171,7 @@
   25.22  (*** is_recfun ***)
   25.23  
   25.24  Goalw [is_recfun_def,cut_def]
   25.25 -    "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
   25.26 +    "[| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
   25.27  by (etac ssubst 1);
   25.28  by (asm_simp_tac HOL_ss 1);
   25.29  qed "is_recfun_undef";
   25.30 @@ -261,7 +261,7 @@
   25.31                       (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
   25.32  
   25.33  Goalw [wfrec_def]
   25.34 -    "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
   25.35 +    "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
   25.36  by (rtac H_cong 1);
   25.37  by (rtac refl 2);
   25.38  by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
   25.39 @@ -297,7 +297,7 @@
   25.40  
   25.41  (*--------------Old proof-----------------------------------------------------
   25.42  Goalw [wfrec_def]
   25.43 -    "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
   25.44 +    "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
   25.45  by (etac (wf_trancl RS wftrec RS ssubst) 1);
   25.46  by (rtac trans_trancl 1);
   25.47  by (rtac (refl RS H_cong) 1);    (*expose the equality of cuts*)
    26.1 --- a/src/HOL/equalities.ML	Wed Jul 15 14:13:18 1998 +0200
    26.2 +++ b/src/HOL/equalities.ML	Wed Jul 15 14:19:02 1998 +0200
    26.3 @@ -86,7 +86,7 @@
    26.4  	"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
    26.5  
    26.6  Goal
    26.7 -    "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
    26.8 +    "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
    26.9  by (Blast_tac 1);
   26.10  qed "UN_insert_distrib";
   26.11  
   26.12 @@ -477,8 +477,7 @@
   26.13  qed "INT_insert";
   26.14  Addsimps[INT_insert];
   26.15  
   26.16 -Goal
   26.17 -    "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
   26.18 +Goal "A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
   26.19  by (Blast_tac 1);
   26.20  qed "INT_insert_distrib";
   26.21  
    27.1 --- a/src/HOL/ex/MT.ML	Wed Jul 15 14:13:18 1998 +0200
    27.2 +++ b/src/HOL/ex/MT.ML	Wed Jul 15 14:19:02 1998 +0200
    27.3 @@ -27,17 +27,15 @@
    27.4  by (simp_tac (simpset() addsimps prems) 1);
    27.5  qed "infsys_p1";
    27.6  
    27.7 -val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
    27.8 +Goal "P (fst (a,b)) (snd (a,b)) ==> P a b";
    27.9  by (Asm_full_simp_tac 1);
   27.10  qed "infsys_p2";
   27.11  
   27.12 -val prems = goal MT.thy 
   27.13 - "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
   27.14 +Goal "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
   27.15  by (Asm_full_simp_tac 1);
   27.16  qed "infsys_pp1";
   27.17  
   27.18 -val prems = goal MT.thy 
   27.19 - "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
   27.20 +Goal "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
   27.21  by (Asm_full_simp_tac 1);
   27.22  qed "infsys_pp2";
   27.23  
   27.24 @@ -154,51 +152,46 @@
   27.25  by (blast_tac (claset() addSIs [exI]) 1);
   27.26  qed "eval_const";
   27.27  
   27.28 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
   27.29 +Goalw [eval_def, eval_rel_def] 
   27.30    "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
   27.31 -by (cut_facts_tac prems 1);
   27.32  by (rtac lfp_intro2 1);
   27.33  by (rtac eval_fun_mono 1);
   27.34  by (rewtac eval_fun_def);
   27.35  by (blast_tac (claset() addSIs [exI]) 1);
   27.36  qed "eval_var2";
   27.37  
   27.38 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
   27.39 +Goalw [eval_def, eval_rel_def] 
   27.40    "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
   27.41 -by (cut_facts_tac prems 1);
   27.42  by (rtac lfp_intro2 1);
   27.43  by (rtac eval_fun_mono 1);
   27.44  by (rewtac eval_fun_def);
   27.45  by (blast_tac (claset() addSIs [exI]) 1);
   27.46  qed "eval_fn";
   27.47  
   27.48 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
   27.49 +Goalw [eval_def, eval_rel_def] 
   27.50    " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   27.51  \   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
   27.52 -by (cut_facts_tac prems 1);
   27.53  by (rtac lfp_intro2 1);
   27.54  by (rtac eval_fun_mono 1);
   27.55  by (rewtac eval_fun_def);
   27.56  by (blast_tac (claset() addSIs [exI]) 1);
   27.57  qed "eval_fix";
   27.58  
   27.59 -val prems = goalw MT.thy [eval_def, eval_rel_def]
   27.60 +Goalw [eval_def, eval_rel_def]
   27.61    " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
   27.62  \   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
   27.63 -by (cut_facts_tac prems 1);
   27.64  by (rtac lfp_intro2 1);
   27.65  by (rtac eval_fun_mono 1);
   27.66  by (rewtac eval_fun_def);
   27.67  by (blast_tac (claset() addSIs [exI]) 1);
   27.68  qed "eval_app1";
   27.69  
   27.70 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
   27.71 +Goalw [eval_def, eval_rel_def] 
   27.72    " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
   27.73  \       ve |- e2 ---> v2; \
   27.74  \       vem + {xm |-> v2} |- em ---> v \
   27.75  \   |] ==> \
   27.76  \   ve |- e1 @ e2 ---> v";
   27.77 -by (cut_facts_tac prems 1);
   27.78  by (rtac lfp_intro2 1);
   27.79  by (rtac eval_fun_mono 1);
   27.80  by (rewtac eval_fun_def);
   27.81 @@ -270,7 +263,7 @@
   27.82  (* Introduction rules *)
   27.83  
   27.84  Goalw [elab_def, elab_rel_def] 
   27.85 -  "!!te. c isof ty ==> te |- e_const(c) ===> ty";
   27.86 +  "c isof ty ==> te |- e_const(c) ===> ty";
   27.87  by (rtac lfp_intro2 1);
   27.88  by (rtac elab_fun_mono 1);
   27.89  by (rewtac elab_fun_def);
   27.90 @@ -278,7 +271,7 @@
   27.91  qed "elab_const";
   27.92  
   27.93  Goalw [elab_def, elab_rel_def] 
   27.94 -  "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
   27.95 +  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
   27.96  by (rtac lfp_intro2 1);
   27.97  by (rtac elab_fun_mono 1);
   27.98  by (rewtac elab_fun_def);
   27.99 @@ -286,7 +279,7 @@
  27.100  qed "elab_var";
  27.101  
  27.102  Goalw [elab_def, elab_rel_def] 
  27.103 -  "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
  27.104 +  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
  27.105  by (rtac lfp_intro2 1);
  27.106  by (rtac elab_fun_mono 1);
  27.107  by (rewtac elab_fun_def);
  27.108 @@ -294,7 +287,7 @@
  27.109  qed "elab_fn";
  27.110  
  27.111  Goalw [elab_def, elab_rel_def]
  27.112 -  "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
  27.113 +  "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
  27.114  \        te |- fix f(x) = e ===> ty1->ty2";
  27.115  by (rtac lfp_intro2 1);
  27.116  by (rtac elab_fun_mono 1);
  27.117 @@ -303,7 +296,7 @@
  27.118  qed "elab_fix";
  27.119  
  27.120  Goalw [elab_def, elab_rel_def] 
  27.121 -  "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
  27.122 +  "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
  27.123  \        te |- e1 @ e2 ===> ty2";
  27.124  by (rtac lfp_intro2 1);
  27.125  by (rtac elab_fun_mono 1);
  27.126 @@ -425,8 +418,7 @@
  27.127  by (elab_e_elim_tac prems);
  27.128  qed "elab_const_elim_lem";
  27.129  
  27.130 -val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
  27.131 -by (cut_facts_tac prems 1);
  27.132 +Goal "te |- e_const(c) ===> t ==> c isof t";
  27.133  by (dtac elab_const_elim_lem 1);
  27.134  by (Blast_tac 1);
  27.135  qed "elab_const_elim";
  27.136 @@ -436,9 +428,7 @@
  27.137  by (elab_e_elim_tac prems);
  27.138  qed "elab_var_elim_lem";
  27.139  
  27.140 -val prems = goal MT.thy 
  27.141 -  "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
  27.142 -by (cut_facts_tac prems 1);
  27.143 +Goal "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
  27.144  by (dtac elab_var_elim_lem 1);
  27.145  by (Blast_tac 1);
  27.146  qed "elab_var_elim";
  27.147 @@ -451,10 +441,9 @@
  27.148  by (elab_e_elim_tac prems);
  27.149  qed "elab_fn_elim_lem";
  27.150  
  27.151 -val prems = goal MT.thy 
  27.152 +Goal 
  27.153    " te |- fn x1 => e1 ===> t ==> \
  27.154  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
  27.155 -by (cut_facts_tac prems 1);
  27.156  by (dtac elab_fn_elim_lem 1);
  27.157  by (Blast_tac 1);
  27.158  qed "elab_fn_elim";
  27.159 @@ -466,10 +455,9 @@
  27.160  by (elab_e_elim_tac prems);
  27.161  qed "elab_fix_elim_lem";
  27.162  
  27.163 -val prems = goal MT.thy 
  27.164 +Goal 
  27.165    " te |- fix ev1(ev2) = e1 ===> t ==> \
  27.166  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
  27.167 -by (cut_facts_tac prems 1);
  27.168  by (dtac elab_fix_elim_lem 1);
  27.169  by (Blast_tac 1);
  27.170  qed "elab_fix_elim";
  27.171 @@ -480,9 +468,8 @@
  27.172  by (elab_e_elim_tac prems);
  27.173  qed "elab_app_elim_lem";
  27.174  
  27.175 -val prems = goal MT.thy
  27.176 +Goal
  27.177   "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
  27.178 -by (cut_facts_tac prems 1);
  27.179  by (dtac elab_app_elim_lem 1);
  27.180  by (Blast_tac 1);
  27.181  qed "elab_app_elim";
  27.182 @@ -505,9 +492,7 @@
  27.183  
  27.184  (* First strong indtroduction (co-induction) rule for hasty_rel *)
  27.185  
  27.186 -val prems =
  27.187  Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
  27.188 -by (cut_facts_tac prems 1);
  27.189  by (rtac gfp_coind2 1);
  27.190  by (rewtac MT.hasty_fun_def);
  27.191  by (rtac CollectI 1);
  27.192 @@ -518,7 +503,7 @@
  27.193  
  27.194  (* Second strong introduction (co-induction) rule for hasty_rel *)
  27.195  
  27.196 -val prems = goalw MT.thy [hasty_rel_def]
  27.197 +Goalw [hasty_rel_def]
  27.198    " [|  te |- fn ev => e ===> t; \
  27.199  \       ve_dom(ve) = te_dom(te); \
  27.200  \       ! ev1. \
  27.201 @@ -526,7 +511,6 @@
  27.202  \         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
  27.203  \   |] ==> \
  27.204  \   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
  27.205 -by (cut_facts_tac prems 1);
  27.206  by (rtac gfp_coind2 1);
  27.207  by (rewtac hasty_fun_def);
  27.208  by (rtac CollectI 1);
  27.209 @@ -579,7 +563,7 @@
  27.210  qed "hasty_const";
  27.211  
  27.212  Goalw [hasty_def,hasty_env_def] 
  27.213 - "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
  27.214 + "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
  27.215  by (rtac hasty_rel_clos_coind 1);
  27.216  by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
  27.217  qed "hasty_clos";
  27.218 @@ -587,7 +571,7 @@
  27.219  (* Elimination on constants for hasty *)
  27.220  
  27.221  Goalw [hasty_def] 
  27.222 -  "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
  27.223 +  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
  27.224  by (rtac hasty_rel_elim 1);
  27.225  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
  27.226  qed "hasty_elim_const_lem";
  27.227 @@ -599,17 +583,16 @@
  27.228  
  27.229  (* Elimination on closures for hasty *)
  27.230  
  27.231 -val prems = goalw MT.thy [hasty_env_def,hasty_def] 
  27.232 +Goalw [hasty_env_def,hasty_def] 
  27.233    " v hasty t ==> \
  27.234  \   ! x e ve. \
  27.235  \     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
  27.236 -by (cut_facts_tac prems 1);
  27.237  by (rtac hasty_rel_elim 1);
  27.238  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
  27.239  qed "hasty_elim_clos_lem";
  27.240  
  27.241  Goal 
  27.242 -  "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
  27.243 +  "v_clos(<|ev,e,ve|>) hasty t ==>  \
  27.244  \       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
  27.245  by (dtac hasty_elim_clos_lem 1);
  27.246  by (Blast_tac 1);
  27.247 @@ -620,7 +603,7 @@
  27.248  (* ############################################################ *)
  27.249  
  27.250  Goal
  27.251 -  "!!ve. [| ve hastyenv te; v hasty t |] ==> \
  27.252 +  "[| ve hastyenv te; v hasty t |] ==> \
  27.253  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
  27.254  by (rewtac hasty_env_def);
  27.255  by (asm_full_simp_tac (simpset() delsimps mem_simps
  27.256 @@ -637,27 +620,27 @@
  27.257  (* ############################################################ *)
  27.258  
  27.259  Goal 
  27.260 -  "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
  27.261 +  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
  27.262  by (dtac elab_const_elim 1);
  27.263  by (etac hasty_const 1);
  27.264  qed "consistency_const";
  27.265  
  27.266  Goalw [hasty_env_def]
  27.267 -  "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
  27.268 +  "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
  27.269  \       ve_app ve ev hasty t";
  27.270  by (dtac elab_var_elim 1);
  27.271  by (Blast_tac 1);
  27.272  qed "consistency_var";
  27.273  
  27.274  Goal
  27.275 -  "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
  27.276 +  "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
  27.277  \       v_clos(<| ev, e, ve |>) hasty t";
  27.278  by (rtac hasty_clos 1);
  27.279  by (Blast_tac 1);
  27.280  qed "consistency_fn";
  27.281  
  27.282  Goalw [hasty_env_def,hasty_def]
  27.283 -  "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
  27.284 +  "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
  27.285  \      ve hastyenv te ; \
  27.286  \      te |- fix ev2  ev1  = e ===> t \
  27.287  \   |] ==> \
  27.288 @@ -684,7 +667,7 @@
  27.289  qed "consistency_fix";
  27.290  
  27.291  Goal 
  27.292 -  "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
  27.293 +  "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
  27.294  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
  27.295  \      ve hastyenv te ; te |- e1 @ e2 ===> t \
  27.296  \   |] ==> \
  27.297 @@ -700,7 +683,7 @@
  27.298  qed "consistency_app1";
  27.299  
  27.300  Goal 
  27.301 -  "!!t.  [| ! t te. \
  27.302 +  "[| ! t te. \
  27.303  \        ve hastyenv te  --> \
  27.304  \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
  27.305  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
  27.306 @@ -726,13 +709,13 @@
  27.307  by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
  27.308  qed "consistency_app2";
  27.309  
  27.310 -val [major] = goal MT.thy 
  27.311 +Goal
  27.312    "ve |- e ---> v ==> \
  27.313  \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
  27.314  
  27.315  (* Proof by induction on the structure of evaluations *)
  27.316  
  27.317 -by (rtac (major RS eval_ind) 1);
  27.318 +by (etac eval_ind 1);
  27.319  by Safe_tac;
  27.320  by (DEPTH_SOLVE 
  27.321      (ares_tac [consistency_const, consistency_var, consistency_fn,
  27.322 @@ -743,9 +726,8 @@
  27.323  (* The Basic Consistency theorem                                *)
  27.324  (* ############################################################ *)
  27.325  
  27.326 -val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
  27.327 +Goalw [isof_env_def,hasty_env_def] 
  27.328    "ve isofenv te ==> ve hastyenv te";
  27.329 -by (cut_facts_tac prems 1);
  27.330  by Safe_tac;
  27.331  by (etac allE 1);
  27.332  by (etac impE 1);
  27.333 @@ -756,9 +738,8 @@
  27.334  by (Asm_simp_tac 1);
  27.335  qed "basic_consistency_lem";
  27.336  
  27.337 -val prems = goal MT.thy
  27.338 +Goal
  27.339    "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
  27.340 -by (cut_facts_tac prems 1);
  27.341  by (rtac hasty_elim_const 1);
  27.342  by (dtac consistency 1);
  27.343  by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
    28.1 --- a/src/HOL/ex/Primes.ML	Wed Jul 15 14:13:18 1998 +0200
    28.2 +++ b/src/HOL/ex/Primes.ML	Wed Jul 15 14:19:02 1998 +0200
    28.3 @@ -90,7 +90,7 @@
    28.4  
    28.5  (*USED??*)
    28.6  Goalw [is_gcd_def]
    28.7 -    "!!m n. [| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
    28.8 +    "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
    28.9  by (Blast_tac 1);
   28.10  qed "is_gcd_dvd";
   28.11  
    29.1 --- a/src/HOL/ex/Primrec.ML	Wed Jul 15 14:13:18 1998 +0200
    29.2 +++ b/src/HOL/ex/Primrec.ML	Wed Jul 15 14:19:02 1998 +0200
    29.3 @@ -195,9 +195,8 @@
    29.4  
    29.5  (** COMP case **)
    29.6  
    29.7 -Goal
    29.8 - "!!fs. fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
    29.9 -\      ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
   29.10 +Goal "fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   29.11 +\     ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
   29.12  by (etac lists.induct 1);
   29.13  by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
   29.14  by Safe_tac;
   29.15 @@ -206,9 +205,9 @@
   29.16  qed "COMP_map_lemma";
   29.17  
   29.18  Goalw [COMP_def]
   29.19 - "!!g. [| ALL l. g l < ack(kg, list_add l);           \
   29.20 -\         fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   29.21 -\      |] ==> EX k. ALL l. COMP g fs  l < ack(k, list_add l)";
   29.22 + "[| ALL l. g l < ack(kg, list_add l);           \
   29.23 +\    fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   29.24 +\ |] ==> EX k. ALL l. COMP g fs  l < ack(k, list_add l)";
   29.25  by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1);
   29.26  by (etac (COMP_map_lemma RS exE) 1);
   29.27  by (rtac exI 1);
   29.28 @@ -221,9 +220,9 @@
   29.29  (** PREC case **)
   29.30  
   29.31  Goalw [PREC_def]
   29.32 - "!!f g. [| ALL l. f l + list_add l < ack(kf, list_add l); \
   29.33 -\           ALL l. g l + list_add l < ack(kg, list_add l)  \
   29.34 -\        |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
   29.35 + "[| ALL l. f l + list_add l < ack(kf, list_add l); \
   29.36 +\    ALL l. g l + list_add l < ack(kg, list_add l)  \
   29.37 +\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
   29.38  by (exhaust_tac "l" 1);
   29.39  by (ALLGOALS Asm_simp_tac);
   29.40  by (blast_tac (claset() addIs [less_trans]) 1);
   29.41 @@ -244,10 +243,9 @@
   29.42  by (etac ack_less_mono2 1);
   29.43  qed "PREC_case_lemma";
   29.44  
   29.45 -Goal
   29.46 - "!!f g. [| ALL l. f l < ack(kf, list_add l);        \
   29.47 -\           ALL l. g l < ack(kg, list_add l)         \
   29.48 -\        |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
   29.49 +Goal "[| ALL l. f l < ack(kf, list_add l);        \
   29.50 +\        ALL l. g l < ack(kg, list_add l)         \
   29.51 +\     |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
   29.52  by (rtac exI 1);
   29.53  by (rtac allI 1);
   29.54  by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
    30.1 --- a/src/HOL/ex/Qsort.ML	Wed Jul 15 14:13:18 1998 +0200
    30.2 +++ b/src/HOL/ex/Qsort.ML	Wed Jul 15 14:19:02 1998 +0200
    30.3 @@ -49,8 +49,7 @@
    30.4  qed "sorted_append";
    30.5  Addsimps [sorted_append];
    30.6  
    30.7 -Goal 
    30.8 - "!!le. [| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
    30.9 +Goal "[| total(le); transf(le) |] ==>  sorted le (qsort le xs)";
   30.10  by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
   30.11  by (ALLGOALS Asm_simp_tac);
   30.12  by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);