# HG changeset patch
# User nipkow
# Date 899455024 -7200
# Node ID 6b995dad8a9d96a5b078f9c6f8f9acd3dd007885
# Parent  7b5efef2ca7434fb62f700d958d9d28eee48a0de
Removed leading !! in goals.

diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -49,7 +49,7 @@
 
 (*** gcd ***)
 
-Goalw [gcd_def] "!!n. 0<n ==> n = gcd n n";
+Goalw [gcd_def] "0<n ==> n = gcd n n";
 by (forward_tac [cd_nnn] 1);
 by (rtac (select_equality RS sym) 1);
 by (blast_tac (claset() addDs [cd_le]) 1);
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -17,7 +17,7 @@
 
 val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end;
 
-Goalw [chop_def] "!!splitf. reducing splitf ==> \
+Goalw [chop_def] "reducing splitf ==> \
 \ chop splitf xs = (let (pre,post) = splitf xs \
 \                   in if pre=[] then ([],xs) \
 \                      else let (xss,zs) = chop splitf post \
@@ -27,11 +27,11 @@
 qed "chop_rule";
 
 Goalw [is_maxsplitter_def,reducing_def]
- "!!splitf. is_maxsplitter P splitf ==> reducing splitf";
+ "is_maxsplitter P splitf ==> reducing splitf";
 by(Asm_full_simp_tac 1);
 qed "is_maxsplitter_reducing";
 
-Goal "!!P. is_maxsplitter P splitf ==> \
+Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
 by(res_inst_tac [("xs","xs")] length_induct 1);
 by(asm_simp_tac (simpset() delsplits [split_if]
@@ -41,7 +41,7 @@
                                 addsplits [split_split]) 1);
 qed_spec_mp "chop_concat";
 
-Goal "!!P. is_maxsplitter P splitf ==> \
+Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
 by(res_inst_tac [("xs","xs")] length_induct 1);
 by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -50,7 +50,7 @@
 Addsplits [split_if];
 
 Goalw [is_maxpref_def]
- "!!P. ~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
+ "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
 by(Blast_tac 1);
 qed "is_maxpref_Nil";
 Addsimps [is_maxpref_Nil];
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/NAe.ML
--- a/src/HOL/Lex/NAe.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/NAe.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -4,15 +4,13 @@
     Copyright   1998 TUM
 *)
 
-Goal
- "steps A w O (eps A)^* = steps A w";
+Goal "steps A w O (eps A)^* = steps A w";
 by (exhaust_tac "w" 1);
 by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
 qed_spec_mp "steps_epsclosure";
 Addsimps [steps_epsclosure];
 
-Goal
- "!! A. [| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
+Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
 by(rtac (steps_epsclosure RS equalityE) 1);
 by(Blast_tac 1);
 qed "in_steps_epsclosure";
@@ -23,14 +21,12 @@
 by (asm_simp_tac (simpset() addsimps [O_assoc RS sym]) 1);
 qed "epsclosure_steps";
 
-Goal
- "!!A. [| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
+Goal "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
 by(rtac (epsclosure_steps RS equalityE) 1);
 by(Blast_tac 1);
 qed "in_epsclosure_steps";
 
-Goal
- "steps A (v@w) = steps A w  O  steps A v";
+Goal "steps A (v@w) = steps A w  O  steps A v";
 by (induct_tac "v" 1);
 by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
 qed "steps_append";
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -74,7 +74,7 @@
 AddIffs
  [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
 
-Goalw [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
+Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
 by(Clarify_tac 1);
 by (Simp_tac 1);
 qed "prefix_prefix";
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -31,23 +31,20 @@
 qed "in_step_atom_Some";
 Addsimps [in_step_atom_Some];
 
-Goal
- "([False],[False]) : steps (atom a) w = (w = [])";
+Goal "([False],[False]) : steps (atom a) w = (w = [])";
 by (induct_tac "w" 1);
  by(Simp_tac 1);
 by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
 qed "False_False_in_steps_atom";
 
-Goal
- "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
+Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
 by (induct_tac "w" 1);
  by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
 by(asm_full_simp_tac (simpset()
      addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
 qed "start_fin_in_steps_atom";
 
-Goal
- "accepts (atom a) w = (w = [a])";
+Goal "accepts (atom a) w = (w = [a])";
 by(simp_tac(simpset() addsimps
        [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
 qed "accepts_atom";
@@ -90,7 +87,7 @@
 (***** True/False ueber epsclosure anheben *****)
 
 Goal
- "!!d. (tp,tq) : (eps(union L R))^* ==> \
+ "(tp,tq) : (eps(union L R))^* ==> \
 \ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
 be rtrancl_induct 1;
  by(Blast_tac 1);
@@ -100,7 +97,7 @@
 val lemma1a = result();
 
 Goal
- "!!d. (tp,tq) : (eps(union L R))^* ==> \
+ "(tp,tq) : (eps(union L R))^* ==> \
 \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
 be rtrancl_induct 1;
  by(Blast_tac 1);
@@ -110,14 +107,14 @@
 val lemma1b = result();
 
 Goal
- "!!p. (p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
+ "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
 be rtrancl_induct 1;
  by(Blast_tac 1);
 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2a = result();
 
 Goal
- "!!p. (p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
+ "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
 be rtrancl_induct 1;
  by(Blast_tac 1);
 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
@@ -291,7 +288,7 @@
 (** False in epsclosure **)
 
 Goal
- "!!d. (tp,tq) : (eps(conc L R))^* ==> \
+ "(tp,tq) : (eps(conc L R))^* ==> \
 \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
 by(etac rtrancl_induct 1);
  by(Blast_tac 1);
@@ -299,7 +296,7 @@
 qed "lemma1b";
 
 Goal
- "!!p. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
+ "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
 by(etac rtrancl_induct 1);
  by(Blast_tac 1);
 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
@@ -329,14 +326,14 @@
 (** True in epsclosure **)
 
 Goal
- "!!L R. (p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
+ "(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
 be rtrancl_induct 1;
  by(Blast_tac 1);
 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 qed "True_True_eps_concI";
 
 Goal
- "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
+ "!p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
 by(induct_tac "w" 1);
  by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
 by (Simp_tac 1);
@@ -344,7 +341,7 @@
 qed_spec_mp "True_True_steps_concI";
 
 Goal
- "!!d. (tp,tq) : (eps(conc L R))^* ==> \
+ "(tp,tq) : (eps(conc L R))^* ==> \
 \ !p. tp = True#p --> \
 \ (? q. tq = True#q & (p,q) : (eps L)^*) | \
 \ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
@@ -354,7 +351,7 @@
 val lemma1a = result();
 
 Goal
- "!!p. (p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
+ "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
 by(etac rtrancl_induct 1);
  by(Blast_tac 1);
 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
@@ -367,7 +364,7 @@
 val lemma = result();
 
 Goal
- "!!L R. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
+ "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
 by(etac rtrancl_induct 1);
  by(Blast_tac 1);
 by (dtac lemma 1);
@@ -477,7 +474,7 @@
 qed_spec_mp "True_True_step_starI";
 
 Goal
-  "!!A. (p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
+  "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
 be rtrancl_induct 1;
  by(Blast_tac 1);
 by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
@@ -489,7 +486,7 @@
 qed_spec_mp "True_start_eps_starI";
 
 Goal
- "!!dummy. (tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> \
+ "(tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> \
 \ (? r. ((p,r) : (eps A)^* | \
 \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
 \       s = True#r))";
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -187,29 +187,29 @@
 qed_spec_mp "regset_spec";
 
 Goalw [bounded_def]
- "!!d. bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)";
+ "bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)";
 by (induct_tac "xs" 1);
  by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "trace_below";
 
-Goal "!!d. [| bounded d k; i < k; j < k |] ==> \
-\         regset d i j k = {xs. deltas d xs i = j}";
+Goal "[| bounded d k; i < k; j < k |] ==> \
+\     regset d i j k = {xs. deltas d xs i = j}";
 by (rtac set_ext 1);
 by (simp_tac (simpset() addsimps [regset_spec]) 1);
 by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
 qed "regset_below";
 
 Goalw [bounded_def]
- "!!d. bounded d k ==> !i. i < k --> deltas d w i < k";
+ "bounded d k ==> !i. i < k --> deltas d w i < k";
 by (induct_tac "w" 1);
  by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "deltas_below";
 
 Goalw [regset_of_DA_def]
- "!!d. [| bounded (next A) k; start A < k; j < k |] ==> \
-\      w : regset_of_DA A k = accepts A w";
+ "[| bounded (next A) k; start A < k; j < k |] ==> \
+\ w : regset_of_DA A k = accepts A w";
 by(asm_simp_tac (simpset() addcongs [conj_cong] addsimps
  [regset_below,deltas_below,accepts_def,delta_def]) 1);
 qed "regset_DA_equiv";
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/MiniML/Generalize.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -6,12 +6,12 @@
 
 AddSEs [equalityE];
 
-Goal "!!A B. free_tv A = free_tv B ==> gen A t = gen B t";
+Goal "free_tv A = free_tv B ==> gen A t = gen B t";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "gen_eq_on_free_tv";
 
-Goal "!!t.(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
+Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
 by (typ.induct_tac "t" 1);
 by (Asm_simp_tac 1);
 by (Simp_tac 1);
@@ -20,7 +20,7 @@
 
 Addsimps [gen_without_effect];
 
-Goal "!!A. free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
+Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv ($ S A)" 1);
@@ -34,14 +34,14 @@
 
 Addsimps [free_tv_gen];
 
-Goal "!!A. free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
+Goal "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "free_tv_gen_cons";
 
 Addsimps [free_tv_gen_cons];
 
-Goal "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
+Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
 by (typ.induct_tac "t1" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
@@ -54,7 +54,7 @@
 
 Addsimps [bound_tv_gen];
 
-Goal "!!A. new_tv n t --> new_tv n (gen A t)";
+Goal "new_tv n t --> new_tv n (gen A t)";
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
@@ -62,14 +62,14 @@
 by (Asm_simp_tac 1);
 qed_spec_mp "new_tv_compatible_gen";
 
-Goalw [gen_ML_def] "!!A. gen A t = gen_ML A t";
+Goalw [gen_ML_def] "gen A t = gen_ML A t";
 by (typ.induct_tac "t" 1);
 by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 qed "gen_eq_gen_ML";
 
-Goal "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
-\          --> gen ($ S A) ($ S t) = $ S (gen A t)";
+Goal "(free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
+\     --> gen ($ S A) ($ S t) = $ S (gen A t)";
 by (induct_tac "t" 1);
  by (strip_tac 1);
  by (case_tac "nat:(free_tv A)" 1);
@@ -102,7 +102,7 @@
 qed "gen_bound_typ_instance";
 
 Goalw [le_type_scheme_def,is_bound_typ_instance]
-  "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
+  "free_tv B <= free_tv A ==> gen A t <= gen B t";
 by Safe_tac;
 by (rename_tac "S" 1);
 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
@@ -113,7 +113,8 @@
 qed "free_tv_subset_gen_le";
 
 Goalw [le_type_scheme_def,is_bound_typ_instance] 
-      "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
+  "new_tv n A --> \
+\  gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
 by (strip_tac 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/MiniML/Instance.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -16,14 +16,14 @@
 
 Addsimps [bound_typ_inst_mk_scheme];
 
-Goal "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
+Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "bound_typ_inst_composed_subst";
 
 Addsimps [bound_typ_inst_composed_subst];
 
-Goal "!!S. S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'";
+Goal "S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'";
 by (Asm_full_simp_tac 1);
 qed "bound_typ_inst_eq";
 
@@ -31,7 +31,7 @@
 
 (* lemmatas for bound_scheme_inst *)
 
-Goal "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t";
+Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -39,7 +39,7 @@
 
 Addsimps [bound_scheme_inst_mk_scheme];
 
-Goal "!!S. $S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
+Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -77,9 +77,9 @@
 qed_spec_mp "bound_scheme_inst_type";
 
 
-(* lemmatas for subst_to_scheme *)
+(* lemmas for subst_to_scheme *)
 
-Goal "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
+Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
 \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
 by (type_scheme.induct_tac "sch" 1);
 by (simp_tac (simpset() addsimps [leD]) 1);
@@ -87,14 +87,15 @@
 by (Asm_simp_tac 1);
 qed_spec_mp "subst_to_scheme_inverse";
 
-Goal "!!t t'. t = t' ==> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \
-\                            subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'";
+Goal "t = t' ==> \
+\     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \
+\     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'";
 by (Fast_tac 1);
 val aux = result ();
 
 Goal "new_tv n sch --> \
-\        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
-\                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
+\     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
+\      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
 by (type_scheme.induct_tac "sch" 1);
 by (simp_tac (simpset() addsimps [leD]) 1);
 by (Asm_simp_tac 1);
@@ -105,7 +106,8 @@
 (* lemmata for <= *)
 
 Goalw [le_type_scheme_def,is_bound_typ_instance]
-      "!!(sch::type_scheme) sch'. (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)";
+  "!!(sch::type_scheme) sch'. \
+\  (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)";
 by (rtac iffI 1);
 by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); 
 by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1);
@@ -175,7 +177,7 @@
 qed "le_env_Cons";
 AddIffs [le_env_Cons];
 
-Goalw [is_bound_typ_instance]"!!t. t <| sch ==> $S t <| $S sch";
+Goalw [is_bound_typ_instance]"t <| sch ==> $S t <| $S sch";
 by (etac exE 1);
 by (rename_tac "SA" 1);
 by (hyp_subst_tac 1);
@@ -190,12 +192,13 @@
 by (Fast_tac 1);
 qed "S_compatible_le_scheme";
 
-Goalw [le_env_def,app_subst_list] "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A";
+Goalw [le_env_def,app_subst_list]
+ "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A";
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
 by (fast_tac (claset() addSIs [S_compatible_le_scheme]) 1);
 qed "S_compatible_le_scheme_lists";
 
-Goalw [le_type_scheme_def] "!!t.[| t <| sch; sch <= sch' |] ==> t <| sch'";
+Goalw [le_type_scheme_def] "[| t <| sch; sch <= sch' |] ==> t <| sch'";
 by (Fast_tac 1);
 qed "bound_typ_instance_trans";
 
@@ -216,7 +219,8 @@
 qed "bound_typ_instance_BVar";
 AddIffs [bound_typ_instance_BVar];
 
-Goalw [le_type_scheme_def,is_bound_typ_instance] "(sch <= FVar n) = (sch = FVar n)";
+Goalw [le_type_scheme_def,is_bound_typ_instance]
+ "(sch <= FVar n) = (sch = FVar n)";
 by (type_scheme.induct_tac "sch" 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
@@ -240,7 +244,7 @@
 AddIffs [not_BVar_le_Fun];
 
 Goalw [le_type_scheme_def,is_bound_typ_instance]
-  "!!sch1. (sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
+  "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'";
 by (fast_tac (claset() addss simpset()) 1);
 qed "Fun_le_FunD";
 
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -24,9 +24,10 @@
 
 Addsimps [s'_a_equals_s_a];
 
-Goal "!!S.($ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A |- e :: \ 
-\              $ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t) ==> \
-\             $S A |- e :: $S t";
+Goal
+ "$(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) A |- \
+\    e :: $(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) t \
+\ ==> $S A |- e :: $S t";
 
 by (res_inst_tac [("P","%A. A |- e :: $S t")] ssubst 1);
 by (rtac (s'_a_equals_s_a RS sym) 1);
@@ -45,51 +46,47 @@
 by (Asm_full_simp_tac 1);
 qed "alpha_A";
 
-Goal "!!alpha. $ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
+Goal "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 qed "S_o_alpha_typ";
 
-Goal "!!alpha. $ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
+Goal "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 val S_o_alpha_typ' = result ();
 
-Goal "!!alpha. $ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
+Goal "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 qed "S_o_alpha_type_scheme";
 
-Goal "!!alpha. $ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
+Goal "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
 by (list.induct_tac "A" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
 qed "S_o_alpha_type_scheme_list";
 
 Goal "!!A::type_scheme list. \
-\              ($ (%n. if n : free_tv A Un free_tv t \
-\                      then S n else TVar n) \
-\                 A) = \
-\              ($ ((%x. if x : free_tv A Un free_tv t then S x \
-\                       else TVar x) o \
-\                  (%x. if x : free_tv A \
-\                       then x else n + x)) A)";
+\     $ (%n. if n : free_tv A Un free_tv t then S n else TVar n) A = \
+\     $ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o \
+\        (%x. if x : free_tv A then x else n + x)) A";
 by (stac S_o_alpha_type_scheme_list 1);
 by (stac alpha_A 1);
 by (rtac refl 1);
 qed "S'_A_eq_S'_alpha_A";
 
 Goalw [free_tv_subst,dom_def]
-          "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
-\               free_tv A Un free_tv t";
+ "dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
+\ free_tv A Un free_tv t";
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "dom_S'";
 
 Goalw [free_tv_subst,cod_def,subset_def]
-          "!!(A::type_scheme list) (t::typ). \ 
-\              cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
-\              free_tv ($ S A) Un free_tv ($ S t)";
+  "!!(A::type_scheme list) (t::typ). \ 
+\  cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
+\  free_tv ($ S A) Un free_tv ($ S t)";
 by (rtac ballI 1);
 by (etac UN_E 1);
 by (dtac (dom_S' RS subsetD) 1);
@@ -100,14 +97,14 @@
 qed "cod_S'";
 
 Goalw [free_tv_subst]
-          "!!(A::type_scheme list) (t::typ). \
-\               free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
-\               free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)";
+ "!!(A::type_scheme list) (t::typ). \
+\ free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
+\ free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)";
 by (fast_tac (claset() addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1);
 qed "free_tv_S'";
 
 Goal "!!t1::typ. \
-\         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
+\     (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
 \         {x. ? y. x = n + y}";
 by (typ.induct_tac "t1" 1);
 by (Simp_tac 1);
@@ -144,7 +141,7 @@
 by (Fast_tac 1);
 val new_tv_Int_free_tv_empty_scheme = result ();
 
-Goal "!!n. !A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
+Goal "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
 by (rtac allI 1);
 by (list.induct_tac "A" 1);
 by (Simp_tac 1);
@@ -153,7 +150,7 @@
 val new_tv_Int_free_tv_empty_scheme_list = result ();
 
 Goalw [le_type_scheme_def,is_bound_typ_instance] 
-      "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
+   "new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
 by (strip_tac 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
@@ -174,7 +171,7 @@
 
 AddSIs has_type.intrs;
 
-Goal "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
+Goal "A |- e::t ==> !B. A <= B -->  B |- e::t";
 by (etac has_type.induct 1);
    by (simp_tac (simpset() addsimps [le_env_def]) 1);
    by (fast_tac (claset() addEs [bound_typ_instance_trans] addss simpset()) 1);
@@ -184,7 +181,7 @@
 qed_spec_mp "has_type_le_env";
 
 (* has_type is closed w.r.t. substitution *)
-Goal "!!a. A |- e :: t ==> !S. $S A |- e :: $S t";
+Goal "A |- e :: t ==> !S. $S A |- e :: $S t";
 by (etac has_type.induct 1);
 (* case VarI *)
    by (rtac allI 1);
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/MiniML/Type.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -28,14 +28,14 @@
 by (Asm_full_simp_tac 1);
 qed_spec_mp "mk_scheme_injective";
 
-Goal "!!t. free_tv (mk_scheme t) = free_tv t";
+Goal "free_tv (mk_scheme t) = free_tv t";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "free_tv_mk_scheme";
 
 Addsimps [free_tv_mk_scheme];
 
-Goal "!!t. $ S (mk_scheme t) = mk_scheme ($ S t)";
+Goal "$ S (mk_scheme t) = mk_scheme ($ S t)";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_mk_scheme";
@@ -95,7 +95,7 @@
 by (fast_tac (HOL_cs addss simpset()) 1);
 qed "new_tv_Cons";
 
-Goalw [new_tv_def] "!!n. new_tv n TVar";
+Goalw [new_tv_def] "new_tv n TVar";
 by (strip_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
 qed "new_tv_TVar_subst";
@@ -109,14 +109,14 @@
 Addsimps[new_tv_id_subst];
 
 Goal "new_tv n (sch::type_scheme) --> \
-\              $(%k. if k<n then S k else S' k) sch = $S sch";
+\     $(%k. if k<n then S k else S' k) sch = $S sch";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme";
 Addsimps [new_if_subst_type_scheme];
 
 Goal "new_tv n (A::type_scheme list) --> \
-\              $(%k. if k<n then S k else S' k) A = $S A";
+\     $(%k. if k<n then S k else S' k) A = $S A";
 by (list.induct_tac "A" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme_list";
@@ -146,7 +146,7 @@
 qed "free_tv_id_subst";
 Addsimps [free_tv_id_subst];
 
-Goal "!!A. !n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
+Goal "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
@@ -157,7 +157,7 @@
 
 Addsimps [free_tv_nth_A_impl_free_tv_A];
 
-Goal "!!A. !nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
+Goal "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
@@ -172,19 +172,18 @@
    structure the substitutions coincide on the free type variables
    occurring in the type structure *)
 
-Goal "!!S S'. (!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
+Goal "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "typ_substitutions_only_on_free_variables";
 
-Goal
-  "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
+Goal  "(!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
 by (rtac typ_substitutions_only_on_free_variables 1);
 by (simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "eq_free_eq_subst_te";
 
-Goal "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
+Goal "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -192,7 +191,7 @@
 qed_spec_mp "scheme_substitutions_only_on_free_variables";
 
 Goal
-  "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
+  "(!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
 by (rtac scheme_substitutions_only_on_free_variables 1);
 by (simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "eq_free_eq_subst_type_scheme";
@@ -206,11 +205,11 @@
 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (simpset())) 1);
 qed_spec_mp "eq_free_eq_subst_scheme_list";
 
-Goal "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
+Goal "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
 by (Fast_tac 1);
 val weaken_asm_Un = result ();
 
-Goal "!!S S'. (!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
+Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
 by (list.induct_tac "A" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -251,22 +250,22 @@
 qed_spec_mp "eq_subst_scheme_list_eq_free";
 
 Goalw [free_tv_subst] 
-      "!!v. v : cod S ==> v : free_tv S";
+      "v : cod S ==> v : free_tv S";
 by (fast_tac set_cs 1);
 qed "codD";
  
 Goalw [free_tv_subst,dom_def] 
-      "!! x. x ~: free_tv S ==> S x = TVar x";
+      "x ~: free_tv S ==> S x = TVar x";
 by (fast_tac set_cs 1);
 qed "not_free_impl_id";
 
 Goalw [new_tv_def] 
-      "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
+      "[| new_tv n t; m:free_tv t |] ==> m<n";
 by (fast_tac HOL_cs 1 );
 qed "free_tv_le_new_tv";
 
 Goalw [dom_def,cod_def,UNION_def,Bex_def]
-  "!!v. [| v : free_tv(S n); v~=n |] ==> v : cod S";
+  "[| v : free_tv(S n); v~=n |] ==> v : cod S";
 by (Simp_tac 1);
 by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
 by (assume_tac 2);
@@ -275,15 +274,13 @@
 qed "cod_app_subst";
 Addsimps [cod_app_subst];
 
-Goal 
-     "free_tv (S (v::nat)) <= insert v (cod S)";
+Goal "free_tv (S (v::nat)) <= insert v (cod S)";
 by (expand_case_tac "v:dom S" 1);
 by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
 by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
 qed "free_tv_subst_var";
 
-Goal 
-     "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
+Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
 by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
@@ -291,8 +288,7 @@
 by (fast_tac (set_cs addss simpset()) 1);
 qed "free_tv_app_subst_te";     
 
-Goal 
-     "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
+Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
 by (type_scheme.induct_tac "sch" 1);
 (* case FVar n *)
 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
@@ -302,8 +298,7 @@
 by (fast_tac (set_cs addss simpset()) 1);
 qed "free_tv_app_subst_type_scheme";  
 
-Goal 
-     "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
+Goal "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
 by (list.induct_tac "A" 1);
 (* case [] *)
 by (Simp_tac 1);
@@ -326,14 +321,14 @@
 by (rtac free_tv_comp_subst 1);
 qed "free_tv_o_subst";
 
-Goal "!!n. n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
+Goal "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
 by (typ.induct_tac "t" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed_spec_mp "free_tv_of_substitutions_extend_to_types";
 
-Goal "!!n. n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
+Goal "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -341,7 +336,7 @@
 by (Fast_tac 1);
 qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
 
-Goal "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
+Goal "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
 by (list.induct_tac "A" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -366,7 +361,7 @@
 
 (* lemmata for bound_tv *)
 
-Goal "!!t. bound_tv (mk_scheme t) = {}";
+Goal "bound_tv (mk_scheme t) = {}";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "bound_tv_mk_scheme";
@@ -443,7 +438,7 @@
 
 (* all greater variables are also new *)
 Goalw [new_tv_def] 
-  "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
+  "n<=m ==> new_tv n t ==> new_tv m t";
 by Safe_tac;
 by (dtac spec 1);
 by (mp_tac 1);
@@ -451,21 +446,21 @@
 qed "new_tv_le";
 Addsimps [lessI RS less_imp_le RS new_tv_le];
 
-Goal "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t";
+Goal "n<=m ==> new_tv n (t::typ) ==> new_tv m t";
 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
 qed "new_tv_typ_le";
 
-Goal "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
+Goal "n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
 qed "new_scheme_list_le";
 
-Goal "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S";
+Goal "n<=m ==> new_tv n (S::subst) ==> new_tv m S";
 by (asm_simp_tac (simpset() addsimps [new_tv_le]) 1);
 qed "new_tv_subst_le";
 
 (* new_tv property remains if a substitution is applied *)
 Goal
-  "!!n. [| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
+  "[| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_var";
 
@@ -513,7 +508,7 @@
 qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
 
 Goalw [new_tv_def]
-  "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
+  "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
 by (list.induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
@@ -525,15 +520,11 @@
 
 
 (* composition of substitutions preserves new_tv proposition *)
-Goal 
-     "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \
-\           new_tv n (($ R) o S)";
+Goal "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) o S)";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_comp_1";
 
-Goal
-     "!! n. [| new_tv n (S::subst); new_tv n R |] ==>  \ 
-\     new_tv n (%v.$ R (S v))";
+Goal "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (%v.$ R (S v))";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_comp_2";
 
@@ -541,7 +532,7 @@
 
 (* new type variables do not occur freely in a type structure *)
 Goalw [new_tv_def] 
-      "!!n. new_tv n A ==> n~:(free_tv A)";
+      "new_tv n A ==> n~:(free_tv A)";
 by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
 qed "new_tv_not_free_tv";
 Addsimps [new_tv_not_free_tv];
@@ -611,7 +602,7 @@
 
 Addsimps [fresh_variable_type_scheme_lists];
 
-Goal "!!x y. [| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)";
+Goal "[| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)";
 by (REPEAT (etac exE 1));
 by (rename_tac "n1 n2" 1);
 by (res_inst_tac [("x","(max n1 n2)")] exI 1);
@@ -643,8 +634,7 @@
 
 (* mgu does not introduce new type variables *)
 Goalw [new_tv_def] 
-      "!! n. [|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> \
-\            new_tv n u";
+      "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u";
 by (fast_tac (set_cs addDs [mgu_free]) 1);
 qed "mgu_new";
 
@@ -719,14 +709,12 @@
 qed "o_id_subst";
 Addsimps[o_id_subst];
 
-Goal
-  "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
+Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_comp_te";
 
-Goal
-  "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
+Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_comp_type_scheme";
diff -r 7b5efef2ca74 -r 6b995dad8a9d src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Jul 03 10:36:47 1998 +0200
+++ b/src/HOL/MiniML/W.ML	Fri Jul 03 10:37:04 1998 +0200
@@ -33,18 +33,18 @@
 Addsimps [W_var_ge];
 
 Goal
-        "!! s. Some (S,t,m) = W e A n ==> n<=m";
+        "Some (S,t,m) = W e A n ==> n<=m";
 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 qed "W_var_geD";
 
-Goal "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
+Goal "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
 by (dtac W_var_geD 1);
 by (rtac new_scheme_list_le 1);
 by (assume_tac 1);
 by (assume_tac 1);
 qed "new_tv_compatible_W";
 
-Goal "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
+Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
 by (type_scheme.induct_tac "sch" 1);
   by (Asm_full_simp_tac 1);
  by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
@@ -155,7 +155,7 @@
 by (assume_tac 1);
 qed_spec_mp "new_tv_W";
 
-Goal "!!sch. (v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
+Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
 by (type_scheme.induct_tac "sch" 1);
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -254,11 +254,11 @@
               addDs [less_le_trans]) 1);
 qed_spec_mp "free_tv_W"; 
 
-Goal "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
+Goal "(!x. x : A --> x ~: B) ==> A Int B = {}";
 by (Fast_tac 1);
 val weaken_A_Int_B_eq_empty = result();
 
-Goal "!!A. x ~: A | x : B ==> x ~: A - B";
+Goal "x ~: A | x : B ==> x ~: A - B";
 by (Fast_tac 1);
 val weaken_not_elem_A_minus_B = result();
 
@@ -559,7 +559,7 @@
 qed_spec_mp "W_complete_lemma";
 
 Goal
- "!!e. [] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
+ "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
 \                                 (? R. t' = $ R t))";
 by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
                 W_complete_lemma 1);