even more tidying of Goal commands
authorpaulson
Thu Aug 13 18:14:26 1998 +0200 (1998-08-13)
changeset 53167a8975451a89
parent 5315 c9ad6bbf3a34
child 5317 3a9214482762
even more tidying of Goal commands
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Gfp.ML
src/HOL/Integ/Integ.ML
src/HOL/Lfp.ML
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/Ord.ML
src/HOL/Prod.ML
src/HOL/RelPow.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/arith_data.ML
src/HOL/equalities.ML
src/HOL/mono.ML
src/HOL/subset.ML
     1.1 --- a/src/HOL/Arith.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4  qed "add_less_mono";
     1.5  
     1.6  (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
     1.7 -val [lt_mono,le] = goal thy
     1.8 +val [lt_mono,le] = Goal
     1.9       "[| !!i j::nat. i<j ==> f(i) < f(j);       \
    1.10  \        i <= j                                 \
    1.11  \     |] ==> f(i) <= (f(j)::nat)";
    1.12 @@ -331,8 +331,8 @@
    1.13  
    1.14  (*** More results about difference ***)
    1.15  
    1.16 -val [prem] = goal thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.17 -by (rtac (prem RS rev_mp) 1);
    1.18 +Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.19 +by (etac rev_mp 1);
    1.20  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.21  by (ALLGOALS Asm_simp_tac);
    1.22  qed "Suc_diff_n";
    1.23 @@ -411,20 +411,20 @@
    1.24  by (ALLGOALS Asm_simp_tac);
    1.25  qed "le_imp_diff_is_add";
    1.26  
    1.27 -val [prem] = goal thy "m < Suc(n) ==> m-n = 0";
    1.28 -by (rtac (prem RS rev_mp) 1);
    1.29 +Goal "m < Suc(n) ==> m-n = 0";
    1.30 +by (etac rev_mp 1);
    1.31  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.32  by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.33  by (ALLGOALS Asm_simp_tac);
    1.34  qed "less_imp_diff_is_0";
    1.35  
    1.36 -val prems = goal thy "m-n = 0  -->  n-m = 0  -->  m=n";
    1.37 +Goal "m-n = 0  -->  n-m = 0  -->  m=n";
    1.38  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.39  by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
    1.40  qed_spec_mp "diffs0_imp_equal";
    1.41  
    1.42 -val [prem] = goal thy "m<n ==> 0<n-m";
    1.43 -by (rtac (prem RS rev_mp) 1);
    1.44 +Goal "m<n ==> 0<n-m";
    1.45 +by (etac rev_mp 1);
    1.46  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.47  by (ALLGOALS Asm_simp_tac);
    1.48  qed "less_imp_diff_positive";
    1.49 @@ -448,7 +448,7 @@
    1.50  by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
    1.51  qed "zero_induct_lemma";
    1.52  
    1.53 -val prems = goal thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.54 +val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.55  by (rtac (diff_self_eq_0 RS subst) 1);
    1.56  by (rtac (zero_induct_lemma RS mp RS mp) 1);
    1.57  by (REPEAT (ares_tac ([impI,allI]@prems) 1));
     2.1 --- a/src/HOL/Divides.ML	Thu Aug 13 18:07:56 1998 +0200
     2.2 +++ b/src/HOL/Divides.ML	Thu Aug 13 18:14:26 1998 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  (** Less-then properties **)
     2.5  
     2.6  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
     2.7 -goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
     2.8 +Goal "[| 0<n; ~ m<n |] ==> m - n < m";
     2.9  by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    2.10  by (Blast_tac 1);
    2.11  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.12 @@ -200,9 +200,10 @@
    2.13   by (trans_tac 2);
    2.14  by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
    2.15  by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
    2.16 - by (best_tac (claset() addIs [le_trans] 
    2.17 -                       addss (simpset() addsimps [diff_less])) 1);
    2.18 -by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
    2.19 +by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
    2.20 +br le_trans 1;
    2.21 +by (Asm_simp_tac 1);
    2.22 +by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
    2.23  qed "div_le_mono2";
    2.24  
    2.25  Goal "0<n ==> m div n <= m";
     3.1 --- a/src/HOL/Finite.ML	Thu Aug 13 18:07:56 1998 +0200
     3.2 +++ b/src/HOL/Finite.ML	Thu Aug 13 18:14:26 1998 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  section "finite";
     3.5  
     3.6  (*Discharging ~ x:y entails extra work*)
     3.7 -val major::prems = goal Finite.thy 
     3.8 +val major::prems = Goal 
     3.9      "[| finite F;  P({}); \
    3.10  \       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
    3.11  \    |] ==> P(F)";
    3.12 @@ -21,7 +21,7 @@
    3.13  by (REPEAT (ares_tac prems 1));
    3.14  qed "finite_induct";
    3.15  
    3.16 -val major::subs::prems = goal Finite.thy 
    3.17 +val major::subs::prems = Goal 
    3.18      "[| finite F;  F <= A; \
    3.19  \       P({}); \
    3.20  \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    3.21 @@ -35,10 +35,9 @@
    3.22  AddSIs Finites.intrs;
    3.23  
    3.24  (*The union of two finite sets is finite*)
    3.25 -val major::prems = goal Finite.thy
    3.26 -    "[| finite F;  finite G |] ==> finite(F Un G)";
    3.27 -by (rtac (major RS finite_induct) 1);
    3.28 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    3.29 +Goal "[| finite F;  finite G |] ==> finite(F Un G)";
    3.30 +by (etac finite_induct 1);
    3.31 +by (ALLGOALS Asm_simp_tac);
    3.32  qed "finite_UnI";
    3.33  
    3.34  (*Every subset of a finite set is finite*)
    3.35 @@ -76,7 +75,7 @@
    3.36  by (Asm_simp_tac 1);
    3.37  qed "finite_imageI";
    3.38  
    3.39 -val major::prems = goal Finite.thy 
    3.40 +val major::prems = Goal 
    3.41      "[| finite c;  finite b;                                  \
    3.42  \       P(b);                                                   \
    3.43  \       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
    3.44 @@ -87,7 +86,7 @@
    3.45                  (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
    3.46  val lemma = result();
    3.47  
    3.48 -val prems = goal Finite.thy 
    3.49 +val prems = Goal 
    3.50      "[| finite A;                                       \
    3.51  \       P(A);                                           \
    3.52  \       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
    3.53 @@ -134,9 +133,8 @@
    3.54  
    3.55  (** The finite UNION of finite sets **)
    3.56  
    3.57 -val [prem] = goal Finite.thy
    3.58 - "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
    3.59 -by (rtac (prem RS finite_induct) 1);
    3.60 +Goal "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
    3.61 +by (etac finite_induct 1);
    3.62  by (ALLGOALS Asm_simp_tac);
    3.63  bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
    3.64  Addsimps [finite_UnionI];
    3.65 @@ -187,7 +185,7 @@
    3.66  
    3.67  section "Finite cardinality -- 'card'";
    3.68  
    3.69 -goal Set.thy "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
    3.70 +Goal "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
    3.71  by (Blast_tac 1);
    3.72  val Collect_conv_insert = result();
    3.73  
    3.74 @@ -197,9 +195,8 @@
    3.75  qed "card_empty";
    3.76  Addsimps [card_empty];
    3.77  
    3.78 -val [major] = goal Finite.thy
    3.79 -  "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
    3.80 -by (rtac (major RS finite_induct) 1);
    3.81 +Goal "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
    3.82 +by (etac finite_induct 1);
    3.83   by (res_inst_tac [("x","0")] exI 1);
    3.84   by (Simp_tac 1);
    3.85  by (etac exE 1);
     4.1 --- a/src/HOL/Fun.ML	Thu Aug 13 18:07:56 1998 +0200
     4.2 +++ b/src/HOL/Fun.ML	Thu Aug 13 18:14:26 1998 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  by (rtac ext 1 THEN Asm_simp_tac 1);
     4.5  qed "expand_fun_eq";
     4.6  
     4.7 -val prems = goal thy
     4.8 +val prems = Goal
     4.9      "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    4.10  by (rtac (arg_cong RS box_equals) 1);
    4.11  by (REPEAT (resolve_tac (prems@[refl]) 1));
    4.12 @@ -22,11 +22,11 @@
    4.13  
    4.14  (** "Axiom" of Choice, proved using the description operator **)
    4.15  
    4.16 -goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    4.17 +Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
    4.18  by (fast_tac (claset() addEs [selectI]) 1);
    4.19  qed "choice";
    4.20  
    4.21 -goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
    4.22 +Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
    4.23  by (fast_tac (claset() addEs [selectI]) 1);
    4.24  qed "bchoice";
    4.25  
    4.26 @@ -57,44 +57,43 @@
    4.27  
    4.28  (*** inj(f): f is a one-to-one function ***)
    4.29  
    4.30 -val prems = goalw thy [inj_def]
    4.31 +val prems = Goalw [inj_def]
    4.32      "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    4.33  by (blast_tac (claset() addIs prems) 1);
    4.34  qed "injI";
    4.35  
    4.36 -val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)";
    4.37 +val [major] = Goal "(!!x. g(f(x)) = x) ==> inj(f)";
    4.38  by (rtac injI 1);
    4.39  by (etac (arg_cong RS box_equals) 1);
    4.40  by (rtac major 1);
    4.41  by (rtac major 1);
    4.42  qed "inj_inverseI";
    4.43  
    4.44 -val [major,minor] = goalw thy [inj_def]
    4.45 -    "[| inj(f); f(x) = f(y) |] ==> x=y";
    4.46 -by (rtac (major RS spec RS spec RS mp) 1);
    4.47 -by (rtac minor 1);
    4.48 +Goalw [inj_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
    4.49 +by (Blast_tac 1);
    4.50  qed "injD";
    4.51  
    4.52  (*Useful with the simplifier*)
    4.53 -val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)";
    4.54 +Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
    4.55  by (rtac iffI 1);
    4.56 -by (etac (major RS injD) 1);
    4.57 -by (etac arg_cong 1);
    4.58 +by (etac arg_cong 2);
    4.59 +by (etac injD 1);
    4.60 +ba 1;
    4.61  qed "inj_eq";
    4.62  
    4.63 -val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y";
    4.64 -by (rtac (major RS injD) 1);
    4.65 +Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
    4.66 +by (etac injD 1);
    4.67  by (rtac selectI 1);
    4.68  by (rtac refl 1);
    4.69  qed "inj_select";
    4.70  
    4.71  (*A one-to-one function has an inverse (given using select).*)
    4.72 -val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x";
    4.73 -by (EVERY1 [rtac (major RS inj_select)]);
    4.74 +Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
    4.75 +by (etac inj_select 1);
    4.76  qed "inv_f_f";
    4.77  
    4.78  (* Useful??? *)
    4.79 -val [oneone,minor] = goal thy
    4.80 +val [oneone,minor] = Goal
    4.81      "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
    4.82  by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
    4.83  by (rtac (rangeI RS minor) 1);
    4.84 @@ -103,60 +102,52 @@
    4.85  
    4.86  (*** inj_on f A: f is one-to-one over A ***)
    4.87  
    4.88 -val prems = goalw thy [inj_on_def]
    4.89 +val prems = Goalw [inj_on_def]
    4.90      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
    4.91  by (blast_tac (claset() addIs prems) 1);
    4.92  qed "inj_onI";
    4.93  
    4.94 -val [major] = goal thy 
    4.95 +val [major] = Goal 
    4.96      "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
    4.97  by (rtac inj_onI 1);
    4.98  by (etac (apply_inverse RS trans) 1);
    4.99  by (REPEAT (eresolve_tac [asm_rl,major] 1));
   4.100  qed "inj_on_inverseI";
   4.101  
   4.102 -val major::prems = goalw thy [inj_on_def]
   4.103 -    "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   4.104 -by (rtac (major RS bspec RS bspec RS mp) 1);
   4.105 -by (REPEAT (resolve_tac prems 1));
   4.106 +Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   4.107 +by (Blast_tac 1);
   4.108  qed "inj_onD";
   4.109  
   4.110  Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   4.111  by (blast_tac (claset() addSDs [inj_onD]) 1);
   4.112  qed "inj_on_iff";
   4.113  
   4.114 -val major::prems = goal thy
   4.115 -    "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   4.116 -by (rtac contrapos 1);
   4.117 -by (etac (major RS inj_onD) 2);
   4.118 -by (REPEAT (resolve_tac prems 1));
   4.119 +Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   4.120 +by (Blast_tac 1);
   4.121  qed "inj_on_contraD";
   4.122  
   4.123 -Goalw [inj_on_def]
   4.124 -    "[| A<=B; inj_on f B |] ==> inj_on f A";
   4.125 +Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
   4.126  by (Blast_tac 1);
   4.127  qed "subset_inj_on";
   4.128  
   4.129  
   4.130  (*** Lemmas about inj ***)
   4.131  
   4.132 -Goalw [o_def]
   4.133 -    "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
   4.134 +Goalw [o_def] "[| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
   4.135  by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
   4.136  qed "comp_inj";
   4.137  
   4.138 -val [prem] = goal thy "inj(f) ==> inj_on f A";
   4.139 -by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
   4.140 +Goal "inj(f) ==> inj_on f A";
   4.141 +by (blast_tac (claset() addIs [injD, inj_onI]) 1);
   4.142  qed "inj_imp";
   4.143  
   4.144 -val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
   4.145 -by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
   4.146 +Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
   4.147 +by (fast_tac (claset() addIs [selectI]) 1);
   4.148  qed "f_inv_f";
   4.149  
   4.150 -val prems = goal thy
   4.151 -    "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
   4.152 +Goal "[| inv f x=inv f y; x: range(f);  y: range(f) |] ==> x=y";
   4.153  by (rtac (arg_cong RS box_equals) 1);
   4.154 -by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
   4.155 +by (REPEAT (ares_tac [f_inv_f] 1));
   4.156  qed "inv_injective";
   4.157  
   4.158  Goal "[| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
     5.1 --- a/src/HOL/Gfp.ML	Thu Aug 13 18:07:56 1998 +0200
     5.2 +++ b/src/HOL/Gfp.ML	Thu Aug 13 18:14:26 1998 +0200
     5.3 @@ -22,18 +22,18 @@
     5.4  by (etac CollectD 1);
     5.5  qed "gfp_least";
     5.6  
     5.7 -val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
     5.8 +Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
     5.9  by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
    5.10 -            rtac (mono RS monoD), rtac gfp_upperbound, atac]);
    5.11 +            etac monoD, rtac gfp_upperbound, atac]);
    5.12  qed "gfp_lemma2";
    5.13  
    5.14 -val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
    5.15 -by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), 
    5.16 -            rtac gfp_lemma2, rtac mono]);
    5.17 +Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
    5.18 +by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
    5.19 +            etac gfp_lemma2]);
    5.20  qed "gfp_lemma3";
    5.21  
    5.22 -val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
    5.23 -by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
    5.24 +Goal "mono(f) ==> gfp(f) = f(gfp(f))";
    5.25 +by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
    5.26  qed "gfp_Tarski";
    5.27  
    5.28  (*** Coinduction rules for greatest fixed points ***)
    5.29 @@ -70,8 +70,8 @@
    5.30           - instead of the condition  X <= f(X)
    5.31                             consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
    5.32  
    5.33 -val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)";
    5.34 -by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
    5.35 +Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
    5.36 +by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
    5.37  qed "coinduct3_mono_lemma";
    5.38  
    5.39  val [prem,mono] = goal Gfp.thy
    5.40 @@ -88,12 +88,11 @@
    5.41  by (rtac Un_upper2 1);
    5.42  qed "coinduct3_lemma";
    5.43  
    5.44 -val prems = goal Gfp.thy
    5.45 -    "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
    5.46 +Goal
    5.47 +  "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
    5.48  by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
    5.49 -by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
    5.50 -by (rtac (UnI2 RS UnI1) 1);
    5.51 -by (REPEAT (resolve_tac prems 1));
    5.52 +by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1);
    5.53 +by Auto_tac;
    5.54  qed "coinduct3";
    5.55  
    5.56  
    5.57 @@ -111,7 +110,7 @@
    5.58  qed "def_coinduct";
    5.59  
    5.60  (*The version used in the induction/coinduction package*)
    5.61 -val prems = goal Gfp.thy
    5.62 +val prems = Goal
    5.63      "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));  \
    5.64  \       a: X;  !!z. z: X ==> P (X Un A) z |] ==> \
    5.65  \    a : A";
    5.66 @@ -126,7 +125,7 @@
    5.67  qed "def_coinduct3";
    5.68  
    5.69  (*Monotonicity of gfp!*)
    5.70 -val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
    5.71 +val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
    5.72  by (rtac (gfp_upperbound RS gfp_least) 1);
    5.73  by (etac (prem RSN (2,subset_trans)) 1);
    5.74  qed "gfp_mono";
     6.1 --- a/src/HOL/Integ/Integ.ML	Thu Aug 13 18:07:56 1998 +0200
     6.2 +++ b/src/HOL/Integ/Integ.ML	Thu Aug 13 18:14:26 1998 +0200
     6.3 @@ -32,10 +32,8 @@
     6.4  
     6.5  (** Natural deduction for intrel **)
     6.6  
     6.7 -val prems = goalw Integ.thy [intrel_def]
     6.8 -    "[| x1+y2 = x2+y1|] ==> \
     6.9 -\    ((x1,y1),(x2,y2)): intrel";
    6.10 -by (fast_tac (claset() addIs prems) 1);
    6.11 +Goalw  [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
    6.12 +by (Fast_tac 1);
    6.13  qed "intrelI";
    6.14  
    6.15  (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    6.16 @@ -45,7 +43,7 @@
    6.17  by (Fast_tac 1);
    6.18  qed "intrelE_lemma";
    6.19  
    6.20 -val [major,minor] = goal Integ.thy
    6.21 +val [major,minor] = Goal
    6.22    "[| p: intrel;  \
    6.23  \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1|] ==> Q |] \
    6.24  \  ==> Q";
    6.25 @@ -130,8 +128,7 @@
    6.26  qed "zminus";
    6.27  
    6.28  (*by lcp*)
    6.29 -val [prem] = goal Integ.thy
    6.30 -    "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
    6.31 +val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
    6.32  by (res_inst_tac [("x1","z")] 
    6.33      (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
    6.34  by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
    6.35 @@ -159,8 +156,7 @@
    6.36  (**** znegative: the test for negative integers ****)
    6.37  
    6.38  
    6.39 -Goalw [znegative_def, znat_def]
    6.40 -    "~ znegative($# n)";
    6.41 +Goalw [znegative_def, znat_def] "~ znegative($# n)";
    6.42  by (Simp_tac 1);
    6.43  by Safe_tac;
    6.44  qed "not_znegative_znat";
    6.45 @@ -445,13 +441,11 @@
    6.46  by (Simp_tac 1);
    6.47  qed "zminus_zpred";
    6.48  
    6.49 -Goalw [zsuc_def,zpred_def,zdiff_def]
    6.50 -   "zpred(zsuc(z)) = z";
    6.51 +Goalw [zsuc_def,zpred_def,zdiff_def]  "zpred(zsuc(z)) = z";
    6.52  by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
    6.53  qed "zpred_zsuc";
    6.54  
    6.55 -Goalw [zsuc_def,zpred_def,zdiff_def]
    6.56 -   "zsuc(zpred(z)) = z";
    6.57 +Goalw [zsuc_def,zpred_def,zdiff_def]  "zsuc(zpred(z)) = z";
    6.58  by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
    6.59  qed "zsuc_zpred";
    6.60  
    6.61 @@ -473,13 +467,13 @@
    6.62  by (rtac zminus_zminus 1);
    6.63  qed "zminus_exchange";
    6.64  
    6.65 -Goal"(zsuc(z)=zsuc(w)) = (z=w)";
    6.66 +Goal "(zsuc(z)=zsuc(w)) = (z=w)";
    6.67  by Safe_tac;
    6.68  by (dres_inst_tac [("f","zpred")] arg_cong 1);
    6.69  by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
    6.70  qed "bijective_zsuc";
    6.71  
    6.72 -Goal"(zpred(z)=zpred(w)) = (z=w)";
    6.73 +Goal "(zpred(z)=zpred(w)) = (z=w)";
    6.74  by Safe_tac;
    6.75  by (dres_inst_tac [("f","zsuc")] arg_cong 1);
    6.76  by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
    6.77 @@ -579,7 +573,7 @@
    6.78  
    6.79  val zless_zsucI = zlessI RSN (2,zless_trans);
    6.80  
    6.81 -Goal "!!z w::int. z<w ==> ~w<z";
    6.82 +Goal "!!w::int. z<w ==> ~w<z";
    6.83  by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
    6.84  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    6.85  by Safe_tac;
    6.86 @@ -611,7 +605,7 @@
    6.87  by (asm_full_simp_tac
    6.88      (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
    6.89  by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
    6.90 -by (REPEAT (fast_tac (claset() addss (simpset() addsimps add_ac)) 1));
    6.91 +by (auto_tac (claset(), simpset() addsimps add_ac));
    6.92  qed "zless_linear";
    6.93  
    6.94  
    6.95 @@ -664,14 +658,15 @@
    6.96  by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
    6.97  qed "zle_refl";
    6.98  
    6.99 -val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
   6.100 +Goal "[| i <= j; j < k |] ==> i < (k::int)";
   6.101  by (dtac zle_imp_zless_or_eq 1);
   6.102  by (fast_tac (claset() addIs [zless_trans]) 1);
   6.103  qed "zle_zless_trans";
   6.104  
   6.105  Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
   6.106  by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   6.107 -            rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
   6.108 +            rtac zless_or_eq_imp_zle, 
   6.109 +	    fast_tac (claset() addIs [zless_trans])]);
   6.110  qed "zle_trans";
   6.111  
   6.112  Goal "[| z <= w; w <= z |] ==> z = (w::int)";
   6.113 @@ -680,7 +675,7 @@
   6.114  qed "zle_anti_sym";
   6.115  
   6.116  
   6.117 -Goal "!!w w' z::int. z + w' = z + w ==> w' = w";
   6.118 +Goal "!!w::int. z + w' = z + w ==> w' = w";
   6.119  by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
   6.120  by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   6.121  qed "zadd_left_cancel";
   6.122 @@ -688,19 +683,19 @@
   6.123  
   6.124  (*** Monotonicity results ***)
   6.125  
   6.126 -Goal "!!v w z::int. v < w ==> v + z < w + z";
   6.127 +Goal "!!z::int. v < w ==> v + z < w + z";
   6.128  by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
   6.129  by (simp_tac (simpset() addsimps zadd_ac) 1);
   6.130  by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
   6.131  qed "zadd_zless_mono1";
   6.132  
   6.133 -Goal "!!v w z::int. (v+z < w+z) = (v < w)";
   6.134 +Goal "!!z::int. (v+z < w+z) = (v < w)";
   6.135  by (safe_tac (claset() addSEs [zadd_zless_mono1]));
   6.136  by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
   6.137  by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
   6.138  qed "zadd_left_cancel_zless";
   6.139  
   6.140 -Goal "!!v w z::int. (v+z <= w+z) = (v <= w)";
   6.141 +Goal "!!z::int. (v+z <= w+z) = (v <= w)";
   6.142  by (asm_full_simp_tac
   6.143      (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
   6.144  qed "zadd_left_cancel_zle";
   6.145 @@ -709,14 +704,14 @@
   6.146  bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
   6.147  
   6.148  
   6.149 -Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
   6.150 +Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
   6.151  by (etac (zadd_zle_mono1 RS zle_trans) 1);
   6.152  by (simp_tac (simpset() addsimps [zadd_commute]) 1);
   6.153  (*w moves to the end because it is free while z', z are bound*)
   6.154  by (etac zadd_zle_mono1 1);
   6.155  qed "zadd_zle_mono";
   6.156  
   6.157 -Goal "!!w z::int. z<=$#0 ==> w+z <= w";
   6.158 +Goal "!!z::int. z<=$#0 ==> w+z <= w";
   6.159  by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
   6.160  by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1);
   6.161  qed "zadd_zle_self";
   6.162 @@ -726,7 +721,7 @@
   6.163  
   6.164  (** One auxiliary theorem...**)
   6.165  
   6.166 -goal HOL.thy "(x = False) = (~ x)";
   6.167 +Goal "(x = False) = (~ x)";
   6.168    by (fast_tac HOL_cs 1);
   6.169  qed "eq_False_conv";
   6.170  
   6.171 @@ -848,8 +843,7 @@
   6.172  
   6.173  (* a case theorem distinguishing positive and negative int *)  
   6.174  
   6.175 -val prems = goal Integ.thy 
   6.176 -    "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; 
   6.177 +val prems = Goal "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; 
   6.178    by (cut_inst_tac [("P","znegative z")] excluded_middle 1); 
   6.179    by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1); 
   6.180  qed "int_cases"; 
     7.1 --- a/src/HOL/Lfp.ML	Thu Aug 13 18:07:56 1998 +0200
     7.2 +++ b/src/HOL/Lfp.ML	Thu Aug 13 18:14:26 1998 +0200
     7.3 @@ -3,7 +3,7 @@
     7.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.5      Copyright   1992  University of Cambridge
     7.6  
     7.7 -For lfp.thy.  The Knaster-Tarski Theorem
     7.8 +The Knaster-Tarski Theorem
     7.9  *)
    7.10  
    7.11  open Lfp;
    7.12 @@ -12,34 +12,34 @@
    7.13  
    7.14  (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
    7.15  
    7.16 -val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
    7.17 +Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
    7.18  by (rtac (CollectI RS Inter_lower) 1);
    7.19 -by (resolve_tac prems 1);
    7.20 +by (assume_tac 1);
    7.21  qed "lfp_lowerbound";
    7.22  
    7.23 -val prems = goalw Lfp.thy [lfp_def]
    7.24 +val prems = Goalw [lfp_def]
    7.25      "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
    7.26  by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
    7.27  by (etac CollectD 1);
    7.28  qed "lfp_greatest";
    7.29  
    7.30 -val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
    7.31 +Goal "mono(f) ==> f(lfp(f)) <= lfp(f)";
    7.32  by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
    7.33 -            rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
    7.34 +            etac monoD, rtac lfp_lowerbound, atac, atac]);
    7.35  qed "lfp_lemma2";
    7.36  
    7.37 -val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
    7.38 -by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), 
    7.39 -            rtac lfp_lemma2, rtac mono]);
    7.40 +Goal "mono(f) ==> lfp(f) <= f(lfp(f))";
    7.41 +by (EVERY1 [rtac lfp_lowerbound, rtac monoD, assume_tac,
    7.42 +            etac lfp_lemma2]);
    7.43  qed "lfp_lemma3";
    7.44  
    7.45 -val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
    7.46 -by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
    7.47 +Goal "mono(f) ==> lfp(f) = f(lfp(f))";
    7.48 +by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
    7.49  qed "lfp_Tarski";
    7.50  
    7.51  (*** General induction rule for least fixed points ***)
    7.52  
    7.53 -val [lfp,mono,indhyp] = goal Lfp.thy
    7.54 +val [lfp,mono,indhyp] = Goal
    7.55      "[| a: lfp(f);  mono(f);                            \
    7.56  \       !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)   \
    7.57  \    |] ==> P(a)";
    7.58 @@ -62,7 +62,7 @@
    7.59  by (rtac (mono RS lfp_Tarski) 1);
    7.60  qed "def_lfp_Tarski";
    7.61  
    7.62 -val rew::prems = goal Lfp.thy
    7.63 +val rew::prems = Goal
    7.64      "[| A == lfp(f);  mono(f);   a:A;                   \
    7.65  \       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
    7.66  \    |] ==> P(a)";
    7.67 @@ -71,7 +71,7 @@
    7.68  qed "def_induct";
    7.69  
    7.70  (*Monotonicity of lfp!*)
    7.71 -val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
    7.72 +val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)";
    7.73  by (rtac (lfp_lowerbound RS lfp_greatest) 1);
    7.74  by (etac (prem RS subset_trans) 1);
    7.75  qed "lfp_mono";
     8.1 --- a/src/HOL/List.ML	Thu Aug 13 18:07:56 1998 +0200
     8.2 +++ b/src/HOL/List.ML	Thu Aug 13 18:14:26 1998 +0200
     8.3 @@ -8,14 +8,14 @@
     8.4  
     8.5  Goal "!x. xs ~= x#xs";
     8.6  by (induct_tac "xs" 1);
     8.7 -by (Auto_tac);
     8.8 +by Auto_tac;
     8.9  qed_spec_mp "not_Cons_self";
    8.10  bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
    8.11  Addsimps [not_Cons_self,not_Cons_self2];
    8.12  
    8.13  Goal "(xs ~= []) = (? y ys. xs = y#ys)";
    8.14  by (induct_tac "xs" 1);
    8.15 -by (Auto_tac);
    8.16 +by Auto_tac;
    8.17  qed "neq_Nil_conv";
    8.18  
    8.19  (* Induction over the length of a list: *)
    8.20 @@ -71,43 +71,43 @@
    8.21  
    8.22  Goal "length(xs@ys) = length(xs)+length(ys)";
    8.23  by (induct_tac "xs" 1);
    8.24 -by (Auto_tac);
    8.25 +by Auto_tac;
    8.26  qed"length_append";
    8.27  Addsimps [length_append];
    8.28  
    8.29  Goal "length (map f xs) = length xs";
    8.30  by (induct_tac "xs" 1);
    8.31 -by (Auto_tac);
    8.32 +by Auto_tac;
    8.33  qed "length_map";
    8.34  Addsimps [length_map];
    8.35  
    8.36  Goal "length(rev xs) = length(xs)";
    8.37  by (induct_tac "xs" 1);
    8.38 -by (Auto_tac);
    8.39 +by Auto_tac;
    8.40  qed "length_rev";
    8.41  Addsimps [length_rev];
    8.42  
    8.43  Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
    8.44  by (exhaust_tac "xs" 1);
    8.45 -by (Auto_tac);
    8.46 +by Auto_tac;
    8.47  qed "length_tl";
    8.48  Addsimps [length_tl];
    8.49  
    8.50  Goal "(length xs = 0) = (xs = [])";
    8.51  by (induct_tac "xs" 1);
    8.52 -by (Auto_tac);
    8.53 +by Auto_tac;
    8.54  qed "length_0_conv";
    8.55  AddIffs [length_0_conv];
    8.56  
    8.57  Goal "(0 = length xs) = (xs = [])";
    8.58  by (induct_tac "xs" 1);
    8.59 -by (Auto_tac);
    8.60 +by Auto_tac;
    8.61  qed "zero_length_conv";
    8.62  AddIffs [zero_length_conv];
    8.63  
    8.64  Goal "(0 < length xs) = (xs ~= [])";
    8.65  by (induct_tac "xs" 1);
    8.66 -by (Auto_tac);
    8.67 +by Auto_tac;
    8.68  qed "length_greater_0_conv";
    8.69  AddIffs [length_greater_0_conv];
    8.70  
    8.71 @@ -123,36 +123,36 @@
    8.72  
    8.73  Goal "(xs@ys)@zs = xs@(ys@zs)";
    8.74  by (induct_tac "xs" 1);
    8.75 -by (Auto_tac);
    8.76 +by Auto_tac;
    8.77  qed "append_assoc";
    8.78  Addsimps [append_assoc];
    8.79  
    8.80  Goal "xs @ [] = xs";
    8.81  by (induct_tac "xs" 1);
    8.82 -by (Auto_tac);
    8.83 +by Auto_tac;
    8.84  qed "append_Nil2";
    8.85  Addsimps [append_Nil2];
    8.86  
    8.87  Goal "(xs@ys = []) = (xs=[] & ys=[])";
    8.88  by (induct_tac "xs" 1);
    8.89 -by (Auto_tac);
    8.90 +by Auto_tac;
    8.91  qed "append_is_Nil_conv";
    8.92  AddIffs [append_is_Nil_conv];
    8.93  
    8.94  Goal "([] = xs@ys) = (xs=[] & ys=[])";
    8.95  by (induct_tac "xs" 1);
    8.96 -by (Auto_tac);
    8.97 +by Auto_tac;
    8.98  qed "Nil_is_append_conv";
    8.99  AddIffs [Nil_is_append_conv];
   8.100  
   8.101  Goal "(xs @ ys = xs) = (ys=[])";
   8.102  by (induct_tac "xs" 1);
   8.103 -by (Auto_tac);
   8.104 +by Auto_tac;
   8.105  qed "append_self_conv";
   8.106  
   8.107  Goal "(xs = xs @ ys) = (ys=[])";
   8.108  by (induct_tac "xs" 1);
   8.109 -by (Auto_tac);
   8.110 +by Auto_tac;
   8.111  qed "self_append_conv";
   8.112  AddIffs [append_self_conv,self_append_conv];
   8.113  
   8.114 @@ -192,7 +192,7 @@
   8.115  
   8.116  Goal "(xs @ ys = ys) = (xs=[])";
   8.117  by (cut_inst_tac [("zs","[]")] append_same_eq 1);
   8.118 -by (Auto_tac);
   8.119 +by Auto_tac;
   8.120  qed "append_self_conv2";
   8.121  
   8.122  Goal "(ys = xs @ ys) = (xs=[])";
   8.123 @@ -204,13 +204,13 @@
   8.124  
   8.125  Goal "xs ~= [] --> hd xs # tl xs = xs";
   8.126  by (induct_tac "xs" 1);
   8.127 -by (Auto_tac);
   8.128 +by Auto_tac;
   8.129  qed_spec_mp "hd_Cons_tl";
   8.130  Addsimps [hd_Cons_tl];
   8.131  
   8.132  Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
   8.133  by (induct_tac "xs" 1);
   8.134 -by (Auto_tac);
   8.135 +by Auto_tac;
   8.136  qed "hd_append";
   8.137  
   8.138  Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
   8.139 @@ -252,31 +252,31 @@
   8.140  
   8.141  Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
   8.142  by (induct_tac "xs" 1);
   8.143 -by (Auto_tac);
   8.144 +by Auto_tac;
   8.145  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
   8.146  
   8.147  Goal "map (%x. x) = (%xs. xs)";
   8.148  by (rtac ext 1);
   8.149  by (induct_tac "xs" 1);
   8.150 -by (Auto_tac);
   8.151 +by Auto_tac;
   8.152  qed "map_ident";
   8.153  Addsimps[map_ident];
   8.154  
   8.155  Goal "map f (xs@ys) = map f xs @ map f ys";
   8.156  by (induct_tac "xs" 1);
   8.157 -by (Auto_tac);
   8.158 +by Auto_tac;
   8.159  qed "map_append";
   8.160  Addsimps[map_append];
   8.161  
   8.162  Goalw [o_def] "map (f o g) xs = map f (map g xs)";
   8.163  by (induct_tac "xs" 1);
   8.164 -by (Auto_tac);
   8.165 +by Auto_tac;
   8.166  qed "map_compose";
   8.167  Addsimps[map_compose];
   8.168  
   8.169  Goal "rev(map f xs) = map f (rev xs)";
   8.170  by (induct_tac "xs" 1);
   8.171 -by (Auto_tac);
   8.172 +by Auto_tac;
   8.173  qed "rev_map";
   8.174  
   8.175  (* a congruence rule for map: *)
   8.176 @@ -284,19 +284,19 @@
   8.177  by (rtac impI 1);
   8.178  by (hyp_subst_tac 1);
   8.179  by (induct_tac "ys" 1);
   8.180 -by (Auto_tac);
   8.181 +by Auto_tac;
   8.182  val lemma = result();
   8.183  bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
   8.184  
   8.185  Goal "(map f xs = []) = (xs = [])";
   8.186  by (induct_tac "xs" 1);
   8.187 -by (Auto_tac);
   8.188 +by Auto_tac;
   8.189  qed "map_is_Nil_conv";
   8.190  AddIffs [map_is_Nil_conv];
   8.191  
   8.192  Goal "([] = map f xs) = (xs = [])";
   8.193  by (induct_tac "xs" 1);
   8.194 -by (Auto_tac);
   8.195 +by Auto_tac;
   8.196  qed "Nil_is_map_conv";
   8.197  AddIffs [Nil_is_map_conv];
   8.198  
   8.199 @@ -307,25 +307,25 @@
   8.200  
   8.201  Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
   8.202  by (induct_tac "xs" 1);
   8.203 -by (Auto_tac);
   8.204 +by Auto_tac;
   8.205  qed "rev_append";
   8.206  Addsimps[rev_append];
   8.207  
   8.208  Goal "rev(rev l) = l";
   8.209  by (induct_tac "l" 1);
   8.210 -by (Auto_tac);
   8.211 +by Auto_tac;
   8.212  qed "rev_rev_ident";
   8.213  Addsimps[rev_rev_ident];
   8.214  
   8.215  Goal "(rev xs = []) = (xs = [])";
   8.216  by (induct_tac "xs" 1);
   8.217 -by (Auto_tac);
   8.218 +by Auto_tac;
   8.219  qed "rev_is_Nil_conv";
   8.220  AddIffs [rev_is_Nil_conv];
   8.221  
   8.222  Goal "([] = rev xs) = (xs = [])";
   8.223  by (induct_tac "xs" 1);
   8.224 -by (Auto_tac);
   8.225 +by Auto_tac;
   8.226  qed "Nil_is_rev_conv";
   8.227  AddIffs [Nil_is_rev_conv];
   8.228  
   8.229 @@ -341,7 +341,7 @@
   8.230  
   8.231  Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
   8.232  by (res_inst_tac [("xs","xs")] rev_induct 1);
   8.233 -by (Auto_tac);
   8.234 +by Auto_tac;
   8.235  bind_thm ("rev_exhaust",
   8.236    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
   8.237  
   8.238 @@ -352,13 +352,13 @@
   8.239  
   8.240  Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
   8.241  by (induct_tac "xs" 1);
   8.242 -by (Auto_tac);
   8.243 +by Auto_tac;
   8.244  qed "mem_append";
   8.245  Addsimps[mem_append];
   8.246  
   8.247  Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   8.248  by (induct_tac "xs" 1);
   8.249 -by (Auto_tac);
   8.250 +by Auto_tac;
   8.251  qed "mem_filter";
   8.252  Addsimps[mem_filter];
   8.253  
   8.254 @@ -373,40 +373,40 @@
   8.255  
   8.256  Goal "set (xs@ys) = (set xs Un set ys)";
   8.257  by (induct_tac "xs" 1);
   8.258 -by (Auto_tac);
   8.259 +by Auto_tac;
   8.260  qed "set_append";
   8.261  Addsimps[set_append];
   8.262  
   8.263  Goal "(x mem xs) = (x: set xs)";
   8.264  by (induct_tac "xs" 1);
   8.265 -by (Auto_tac);
   8.266 +by Auto_tac;
   8.267  qed "set_mem_eq";
   8.268  
   8.269  Goal "set l <= set (x#l)";
   8.270 -by (Auto_tac);
   8.271 +by Auto_tac;
   8.272  qed "set_subset_Cons";
   8.273  
   8.274  Goal "(set xs = {}) = (xs = [])";
   8.275  by (induct_tac "xs" 1);
   8.276 -by (Auto_tac);
   8.277 +by Auto_tac;
   8.278  qed "set_empty";
   8.279  Addsimps [set_empty];
   8.280  
   8.281  Goal "set(rev xs) = set(xs)";
   8.282  by (induct_tac "xs" 1);
   8.283 -by (Auto_tac);
   8.284 +by Auto_tac;
   8.285  qed "set_rev";
   8.286  Addsimps [set_rev];
   8.287  
   8.288  Goal "set(map f xs) = f``(set xs)";
   8.289  by (induct_tac "xs" 1);
   8.290 -by (Auto_tac);
   8.291 +by Auto_tac;
   8.292  qed "set_map";
   8.293  Addsimps [set_map];
   8.294  
   8.295  Goal "(x : set(filter P xs)) = (x : set xs & P x)";
   8.296  by (induct_tac "xs" 1);
   8.297 -by (Auto_tac);
   8.298 +by Auto_tac;
   8.299  qed "in_set_filter";
   8.300  Addsimps [in_set_filter];
   8.301  
   8.302 @@ -418,14 +418,14 @@
   8.303  by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
   8.304  by(REPEAT(etac exE 1));
   8.305  by(exhaust_tac "ys" 1);
   8.306 -by(Auto_tac);
   8.307 +by Auto_tac;
   8.308  qed "in_set_conv_decomp";
   8.309  
   8.310  (* eliminate `lists' in favour of `set' *)
   8.311  
   8.312  Goal "(xs : lists A) = (!x : set xs. x : A)";
   8.313  by(induct_tac "xs" 1);
   8.314 -by(Auto_tac);
   8.315 +by Auto_tac;
   8.316  qed "in_lists_conv_set";
   8.317  
   8.318  bind_thm("in_listsD",in_lists_conv_set RS iffD1);
   8.319 @@ -439,19 +439,19 @@
   8.320  
   8.321  Goal "list_all (%x. True) xs = True";
   8.322  by (induct_tac "xs" 1);
   8.323 -by (Auto_tac);
   8.324 +by Auto_tac;
   8.325  qed "list_all_True";
   8.326  Addsimps [list_all_True];
   8.327  
   8.328  Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
   8.329  by (induct_tac "xs" 1);
   8.330 -by (Auto_tac);
   8.331 +by Auto_tac;
   8.332  qed "list_all_append";
   8.333  Addsimps [list_all_append];
   8.334  
   8.335  Goal "list_all P xs = (!x. x mem xs --> P(x))";
   8.336  by (induct_tac "xs" 1);
   8.337 -by (Auto_tac);
   8.338 +by Auto_tac;
   8.339  qed "list_all_mem_conv";
   8.340  
   8.341  
   8.342 @@ -461,25 +461,25 @@
   8.343  
   8.344  Goal "filter P (xs@ys) = filter P xs @ filter P ys";
   8.345  by (induct_tac "xs" 1);
   8.346 -by (Auto_tac);
   8.347 +by Auto_tac;
   8.348  qed "filter_append";
   8.349  Addsimps [filter_append];
   8.350  
   8.351  Goal "filter (%x. True) xs = xs";
   8.352  by (induct_tac "xs" 1);
   8.353 -by (Auto_tac);
   8.354 +by Auto_tac;
   8.355  qed "filter_True";
   8.356  Addsimps [filter_True];
   8.357  
   8.358  Goal "filter (%x. False) xs = []";
   8.359  by (induct_tac "xs" 1);
   8.360 -by (Auto_tac);
   8.361 +by Auto_tac;
   8.362  qed "filter_False";
   8.363  Addsimps [filter_False];
   8.364  
   8.365  Goal "length (filter P xs) <= length xs";
   8.366  by (induct_tac "xs" 1);
   8.367 -by (Auto_tac);
   8.368 +by Auto_tac;
   8.369  qed "length_filter";
   8.370  
   8.371  
   8.372 @@ -489,41 +489,41 @@
   8.373  
   8.374  Goal  "concat(xs@ys) = concat(xs)@concat(ys)";
   8.375  by (induct_tac "xs" 1);
   8.376 -by (Auto_tac);
   8.377 +by Auto_tac;
   8.378  qed"concat_append";
   8.379  Addsimps [concat_append];
   8.380  
   8.381  Goal "(concat xss = []) = (!xs:set xss. xs=[])";
   8.382  by (induct_tac "xss" 1);
   8.383 -by (Auto_tac);
   8.384 +by Auto_tac;
   8.385  qed "concat_eq_Nil_conv";
   8.386  AddIffs [concat_eq_Nil_conv];
   8.387  
   8.388  Goal "([] = concat xss) = (!xs:set xss. xs=[])";
   8.389  by (induct_tac "xss" 1);
   8.390 -by (Auto_tac);
   8.391 +by Auto_tac;
   8.392  qed "Nil_eq_concat_conv";
   8.393  AddIffs [Nil_eq_concat_conv];
   8.394  
   8.395  Goal  "set(concat xs) = Union(set `` set xs)";
   8.396  by (induct_tac "xs" 1);
   8.397 -by (Auto_tac);
   8.398 +by Auto_tac;
   8.399  qed"set_concat";
   8.400  Addsimps [set_concat];
   8.401  
   8.402  Goal "map f (concat xs) = concat (map (map f) xs)"; 
   8.403  by (induct_tac "xs" 1);
   8.404 -by (Auto_tac);
   8.405 +by Auto_tac;
   8.406  qed "map_concat";
   8.407  
   8.408  Goal "filter p (concat xs) = concat (map (filter p) xs)"; 
   8.409  by (induct_tac "xs" 1);
   8.410 -by (Auto_tac);
   8.411 +by Auto_tac;
   8.412  qed"filter_concat"; 
   8.413  
   8.414  Goal "rev(concat xs) = concat (map rev (rev xs))";
   8.415  by (induct_tac "xs" 1);
   8.416 -by (Auto_tac);
   8.417 +by Auto_tac;
   8.418  qed "rev_concat";
   8.419  
   8.420  (** nth **)
   8.421 @@ -535,7 +535,7 @@
   8.422   by (Asm_simp_tac 1);
   8.423   by (rtac allI 1);
   8.424   by (exhaust_tac "xs" 1);
   8.425 -  by (Auto_tac);
   8.426 +  by Auto_tac;
   8.427  qed_spec_mp "nth_append";
   8.428  
   8.429  Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
   8.430 @@ -545,7 +545,7 @@
   8.431  (* case x#xl *)
   8.432  by (rtac allI 1);
   8.433  by (induct_tac "n" 1);
   8.434 -by (Auto_tac);
   8.435 +by Auto_tac;
   8.436  qed_spec_mp "nth_map";
   8.437  Addsimps [nth_map];
   8.438  
   8.439 @@ -556,7 +556,7 @@
   8.440  (* case x#xl *)
   8.441  by (rtac allI 1);
   8.442  by (induct_tac "n" 1);
   8.443 -by (Auto_tac);
   8.444 +by Auto_tac;
   8.445  qed_spec_mp "list_all_nth";
   8.446  
   8.447  Goal "!n. n < length xs --> xs!n mem xs";
   8.448 @@ -589,30 +589,30 @@
   8.449  
   8.450  Goal "last(xs@[x]) = x";
   8.451  by (induct_tac "xs" 1);
   8.452 -by (Auto_tac);
   8.453 +by Auto_tac;
   8.454  qed "last_snoc";
   8.455  Addsimps [last_snoc];
   8.456  
   8.457  Goal "butlast(xs@[x]) = xs";
   8.458  by (induct_tac "xs" 1);
   8.459 -by (Auto_tac);
   8.460 +by Auto_tac;
   8.461  qed "butlast_snoc";
   8.462  Addsimps [butlast_snoc];
   8.463  
   8.464  Goal "length(butlast xs) = length xs - 1";
   8.465  by (res_inst_tac [("xs","xs")] rev_induct 1);
   8.466 -by (Auto_tac);
   8.467 +by Auto_tac;
   8.468  qed "length_butlast";
   8.469  Addsimps [length_butlast];
   8.470  
   8.471  Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   8.472  by (induct_tac "xs" 1);
   8.473 -by (Auto_tac);
   8.474 +by Auto_tac;
   8.475  qed_spec_mp "butlast_append";
   8.476  
   8.477  Goal "x:set(butlast xs) --> x:set xs";
   8.478  by (induct_tac "xs" 1);
   8.479 -by (Auto_tac);
   8.480 +by Auto_tac;
   8.481  qed_spec_mp "in_set_butlastD";
   8.482  
   8.483  Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   8.484 @@ -631,12 +631,12 @@
   8.485  
   8.486  Goal "take 0 xs = []";
   8.487  by (induct_tac "xs" 1);
   8.488 -by (Auto_tac);
   8.489 +by Auto_tac;
   8.490  qed "take_0";
   8.491  
   8.492  Goal "drop 0 xs = xs";
   8.493  by (induct_tac "xs" 1);
   8.494 -by (Auto_tac);
   8.495 +by Auto_tac;
   8.496  qed "drop_0";
   8.497  
   8.498  Goal "take (Suc n) (x#xs) = x # take n xs";
   8.499 @@ -652,102 +652,102 @@
   8.500  
   8.501  Goal "!xs. length(take n xs) = min (length xs) n";
   8.502  by (induct_tac "n" 1);
   8.503 - by (Auto_tac);
   8.504 + by Auto_tac;
   8.505  by (exhaust_tac "xs" 1);
   8.506 - by (Auto_tac);
   8.507 + by Auto_tac;
   8.508  qed_spec_mp "length_take";
   8.509  Addsimps [length_take];
   8.510  
   8.511  Goal "!xs. length(drop n xs) = (length xs - n)";
   8.512  by (induct_tac "n" 1);
   8.513 - by (Auto_tac);
   8.514 + by Auto_tac;
   8.515  by (exhaust_tac "xs" 1);
   8.516 - by (Auto_tac);
   8.517 + by Auto_tac;
   8.518  qed_spec_mp "length_drop";
   8.519  Addsimps [length_drop];
   8.520  
   8.521  Goal "!xs. length xs <= n --> take n xs = xs";
   8.522  by (induct_tac "n" 1);
   8.523 - by (Auto_tac);
   8.524 + by Auto_tac;
   8.525  by (exhaust_tac "xs" 1);
   8.526 - by (Auto_tac);
   8.527 + by Auto_tac;
   8.528  qed_spec_mp "take_all";
   8.529  
   8.530  Goal "!xs. length xs <= n --> drop n xs = []";
   8.531  by (induct_tac "n" 1);
   8.532 - by (Auto_tac);
   8.533 + by Auto_tac;
   8.534  by (exhaust_tac "xs" 1);
   8.535 - by (Auto_tac);
   8.536 + by Auto_tac;
   8.537  qed_spec_mp "drop_all";
   8.538  
   8.539  Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   8.540  by (induct_tac "n" 1);
   8.541 - by (Auto_tac);
   8.542 + by Auto_tac;
   8.543  by (exhaust_tac "xs" 1);
   8.544 - by (Auto_tac);
   8.545 + by Auto_tac;
   8.546  qed_spec_mp "take_append";
   8.547  Addsimps [take_append];
   8.548  
   8.549  Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   8.550  by (induct_tac "n" 1);
   8.551 - by (Auto_tac);
   8.552 + by Auto_tac;
   8.553  by (exhaust_tac "xs" 1);
   8.554 - by (Auto_tac);
   8.555 + by Auto_tac;
   8.556  qed_spec_mp "drop_append";
   8.557  Addsimps [drop_append];
   8.558  
   8.559  Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
   8.560  by (induct_tac "m" 1);
   8.561 - by (Auto_tac);
   8.562 + by Auto_tac;
   8.563  by (exhaust_tac "xs" 1);
   8.564 - by (Auto_tac);
   8.565 + by Auto_tac;
   8.566  by (exhaust_tac "na" 1);
   8.567 - by (Auto_tac);
   8.568 + by Auto_tac;
   8.569  qed_spec_mp "take_take";
   8.570  
   8.571  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   8.572  by (induct_tac "m" 1);
   8.573 - by (Auto_tac);
   8.574 + by Auto_tac;
   8.575  by (exhaust_tac "xs" 1);
   8.576 - by (Auto_tac);
   8.577 + by Auto_tac;
   8.578  qed_spec_mp "drop_drop";
   8.579  
   8.580  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   8.581  by (induct_tac "m" 1);
   8.582 - by (Auto_tac);
   8.583 + by Auto_tac;
   8.584  by (exhaust_tac "xs" 1);
   8.585 - by (Auto_tac);
   8.586 + by Auto_tac;
   8.587  qed_spec_mp "take_drop";
   8.588  
   8.589  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
   8.590  by (induct_tac "n" 1);
   8.591 - by (Auto_tac);
   8.592 + by Auto_tac;
   8.593  by (exhaust_tac "xs" 1);
   8.594 - by (Auto_tac);
   8.595 + by Auto_tac;
   8.596  qed_spec_mp "take_map"; 
   8.597  
   8.598  Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
   8.599  by (induct_tac "n" 1);
   8.600 - by (Auto_tac);
   8.601 + by Auto_tac;
   8.602  by (exhaust_tac "xs" 1);
   8.603 - by (Auto_tac);
   8.604 + by Auto_tac;
   8.605  qed_spec_mp "drop_map";
   8.606  
   8.607  Goal "!n i. i < n --> (take n xs)!i = xs!i";
   8.608  by (induct_tac "xs" 1);
   8.609 - by (Auto_tac);
   8.610 + by Auto_tac;
   8.611  by (exhaust_tac "n" 1);
   8.612   by (Blast_tac 1);
   8.613  by (exhaust_tac "i" 1);
   8.614 - by (Auto_tac);
   8.615 + by Auto_tac;
   8.616  qed_spec_mp "nth_take";
   8.617  Addsimps [nth_take];
   8.618  
   8.619  Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
   8.620  by (induct_tac "n" 1);
   8.621 - by (Auto_tac);
   8.622 + by Auto_tac;
   8.623  by (exhaust_tac "xs" 1);
   8.624 - by (Auto_tac);
   8.625 + by Auto_tac;
   8.626  qed_spec_mp "nth_drop";
   8.627  Addsimps [nth_drop];
   8.628  
   8.629 @@ -757,37 +757,37 @@
   8.630  
   8.631  Goal "takeWhile P xs @ dropWhile P xs = xs";
   8.632  by (induct_tac "xs" 1);
   8.633 -by (Auto_tac);
   8.634 +by Auto_tac;
   8.635  qed "takeWhile_dropWhile_id";
   8.636  Addsimps [takeWhile_dropWhile_id];
   8.637  
   8.638  Goal  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   8.639  by (induct_tac "xs" 1);
   8.640 -by (Auto_tac);
   8.641 +by Auto_tac;
   8.642  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   8.643  Addsimps [takeWhile_append1];
   8.644  
   8.645  Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   8.646  by (induct_tac "xs" 1);
   8.647 -by (Auto_tac);
   8.648 +by Auto_tac;
   8.649  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   8.650  Addsimps [takeWhile_append2];
   8.651  
   8.652  Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   8.653  by (induct_tac "xs" 1);
   8.654 -by (Auto_tac);
   8.655 +by Auto_tac;
   8.656  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   8.657  Addsimps [dropWhile_append1];
   8.658  
   8.659  Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   8.660  by (induct_tac "xs" 1);
   8.661 -by (Auto_tac);
   8.662 +by Auto_tac;
   8.663  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   8.664  Addsimps [dropWhile_append2];
   8.665  
   8.666  Goal "x:set(takeWhile P xs) --> x:set xs & P x";
   8.667  by (induct_tac "xs" 1);
   8.668 -by (Auto_tac);
   8.669 +by Auto_tac;
   8.670  qed_spec_mp"set_take_whileD";
   8.671  
   8.672  qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
   8.673 @@ -800,7 +800,7 @@
   8.674  
   8.675  Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
   8.676  by(induct_tac "xs" 1);
   8.677 -by(Auto_tac);
   8.678 +by Auto_tac;
   8.679  qed_spec_mp "foldl_append";
   8.680  Addsimps [foldl_append];
   8.681  
   8.682 @@ -821,7 +821,7 @@
   8.683  
   8.684  Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
   8.685  by(induct_tac "ns" 1);
   8.686 -by(Auto_tac);
   8.687 +by Auto_tac;
   8.688  qed_spec_mp "sum_eq_0_conv";
   8.689  AddIffs [sum_eq_0_conv];
   8.690  
   8.691 @@ -838,12 +838,12 @@
   8.692  
   8.693  Goal "nodups(remdups xs)";
   8.694  by (induct_tac "xs" 1);
   8.695 -by (Auto_tac);
   8.696 +by Auto_tac;
   8.697  qed "nodups_remdups";
   8.698  
   8.699  Goal "nodups xs --> nodups (filter P xs)";
   8.700  by (induct_tac "xs" 1);
   8.701 -by (Auto_tac);
   8.702 +by Auto_tac;
   8.703  qed_spec_mp "nodups_filter";
   8.704  
   8.705  (** replicate **)
   8.706 @@ -851,7 +851,7 @@
   8.707  
   8.708  Goal "set(replicate (Suc n) x) = {x}";
   8.709  by (induct_tac "n" 1);
   8.710 -by (Auto_tac);
   8.711 +by Auto_tac;
   8.712  val lemma = result();
   8.713  
   8.714  Goal "n ~= 0 ==> set(replicate n x) = {x}";
     9.1 --- a/src/HOL/Nat.ML	Thu Aug 13 18:07:56 1998 +0200
     9.2 +++ b/src/HOL/Nat.ML	Thu Aug 13 18:14:26 1998 +0200
     9.3 @@ -9,12 +9,12 @@
     9.4  val [nat_rec_0, nat_rec_Suc] = nat.recs;
     9.5  
     9.6  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
     9.7 -val prems = goal thy
     9.8 +val prems = Goal
     9.9      "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    9.10  by (simp_tac (simpset() addsimps prems) 1);
    9.11  qed "def_nat_rec_0";
    9.12  
    9.13 -val prems = goal thy
    9.14 +val prems = Goal
    9.15      "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    9.16  by (simp_tac (simpset() addsimps prems) 1);
    9.17  qed "def_nat_rec_Suc";
    9.18 @@ -26,9 +26,8 @@
    9.19  by (REPEAT (Blast_tac 1));
    9.20  qed "not0_implies_Suc";
    9.21  
    9.22 -val prems = goal thy "m<n ==> n ~= 0";
    9.23 +Goal "m<n ==> n ~= 0";
    9.24  by (exhaust_tac "n" 1);
    9.25 -by (cut_facts_tac prems 1);
    9.26  by (ALLGOALS Asm_full_simp_tac);
    9.27  qed "gr_implies_not0";
    9.28  
    10.1 --- a/src/HOL/NatDef.ML	Thu Aug 13 18:07:56 1998 +0200
    10.2 +++ b/src/HOL/NatDef.ML	Thu Aug 13 18:14:26 1998 +0200
    10.3 @@ -20,22 +20,22 @@
    10.4  by (rtac (singletonI RS UnI1) 1);
    10.5  qed "Zero_RepI";
    10.6  
    10.7 -val prems = goal thy "i: Nat ==> Suc_Rep(i) : Nat";
    10.8 +Goal "i: Nat ==> Suc_Rep(i) : Nat";
    10.9  by (stac Nat_unfold 1);
   10.10  by (rtac (imageI RS UnI2) 1);
   10.11 -by (resolve_tac prems 1);
   10.12 +by (assume_tac 1);
   10.13  qed "Suc_RepI";
   10.14  
   10.15  (*** Induction ***)
   10.16  
   10.17 -val major::prems = goal thy
   10.18 +val major::prems = Goal
   10.19      "[| i: Nat;  P(Zero_Rep);   \
   10.20  \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
   10.21  by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
   10.22  by (blast_tac (claset() addIs prems) 1);
   10.23  qed "Nat_induct";
   10.24  
   10.25 -val prems = goalw thy [Zero_def,Suc_def]
   10.26 +val prems = Goalw [Zero_def,Suc_def]
   10.27      "[| P(0);   \
   10.28  \       !!n. P(n) ==> P(Suc(n)) |]  ==> P(n)";
   10.29  by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
   10.30 @@ -49,7 +49,7 @@
   10.31    res_inst_tac [("n",a)] nat_induct i  THEN  rename_last_tac a [""] (i+1);
   10.32  
   10.33  (*A special form of induction for reasoning about m<n and m-n*)
   10.34 -val prems = goal thy
   10.35 +val prems = Goal
   10.36      "[| !!x. P x 0;  \
   10.37  \       !!y. P 0 (Suc y);  \
   10.38  \       !!x y. [| P x y |] ==> P (Suc x) (Suc y)  \
   10.39 @@ -131,10 +131,10 @@
   10.40  
   10.41  (** Introduction properties **)
   10.42  
   10.43 -val prems = goalw thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
   10.44 +Goalw [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
   10.45  by (rtac (trans_trancl RS transD) 1);
   10.46 -by (resolve_tac prems 1);
   10.47 -by (resolve_tac prems 1);
   10.48 +by (assume_tac 1);
   10.49 +by (assume_tac 1);
   10.50  qed "less_trans";
   10.51  
   10.52  Goalw [less_def, pred_nat_def] "n < Suc(n)";
   10.53 @@ -156,8 +156,8 @@
   10.54  
   10.55  (** Elimination properties **)
   10.56  
   10.57 -val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
   10.58 -by (blast_tac (claset() addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
   10.59 +Goalw [less_def] "n<m ==> ~ m<(n::nat)";
   10.60 +by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1);
   10.61  qed "less_not_sym";
   10.62  
   10.63  (* [| n<m; m<n |] ==> R *)
   10.64 @@ -176,7 +176,7 @@
   10.65  qed "less_not_refl2";
   10.66  
   10.67  
   10.68 -val major::prems = goalw thy [less_def, pred_nat_def]
   10.69 +val major::prems = Goalw [less_def, pred_nat_def]
   10.70      "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
   10.71  \    |] ==> P";
   10.72  by (rtac (major RS tranclE) 1);
   10.73 @@ -197,7 +197,7 @@
   10.74  (* n<0 ==> R *)
   10.75  bind_thm ("less_zeroE", not_less0 RS notE);
   10.76  
   10.77 -val [major,less,eq] = goal thy
   10.78 +val [major,less,eq] = Goal
   10.79      "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
   10.80  by (rtac (major RS lessE) 1);
   10.81  by (rtac eq 1);
   10.82 @@ -254,14 +254,14 @@
   10.83  by (blast_tac (claset() addSEs [less_irrefl, less_SucE] addEs [less_asym]) 1);
   10.84  qed "Suc_lessI";
   10.85  
   10.86 -val [prem] = goal thy "Suc(m) < n ==> m<n";
   10.87 -by (rtac (prem RS rev_mp) 1);
   10.88 +Goal "Suc(m) < n ==> m<n";
   10.89 +by (etac rev_mp 1);
   10.90  by (nat_ind_tac "n" 1);
   10.91  by (ALLGOALS (fast_tac (claset() addSIs [lessI RS less_SucI]
   10.92                                   addEs  [less_trans, lessE])));
   10.93  qed "Suc_lessD";
   10.94  
   10.95 -val [major,minor] = goal thy 
   10.96 +val [major,minor] = Goal 
   10.97      "[| Suc(i)<k;  !!j. [| i<j;  k=Suc(j) |] ==> P \
   10.98  \    |] ==> P";
   10.99  by (rtac (major RS lessE) 1);
  10.100 @@ -299,7 +299,7 @@
  10.101  qed "not_less_eq";
  10.102  
  10.103  (*Complete induction, aka course-of-values induction*)
  10.104 -val prems = goalw thy [less_def]
  10.105 +val prems = Goalw [less_def]
  10.106      "[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)";
  10.107  by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
  10.108  by (eresolve_tac prems 1);
  10.109 @@ -350,12 +350,12 @@
  10.110  but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
  10.111  *)
  10.112  
  10.113 -val prems = goalw thy [le_def] "~n<m ==> m<=(n::nat)";
  10.114 -by (resolve_tac prems 1);
  10.115 +Goalw [le_def] "~n<m ==> m<=(n::nat)";
  10.116 +by (assume_tac 1);
  10.117  qed "leI";
  10.118  
  10.119 -val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)";
  10.120 -by (resolve_tac prems 1);
  10.121 +Goalw [le_def] "m<=n ==> ~ n < (m::nat)";
  10.122 +by (assume_tac 1);
  10.123  qed "leD";
  10.124  
  10.125  val leE = make_elim leD;
  10.126 @@ -505,7 +505,7 @@
  10.127  by (simp_tac (simpset() addsimps [lemma]) 1);
  10.128  qed "Least_nat_def";
  10.129  
  10.130 -val [prem1,prem2] = goalw thy [Least_nat_def]
  10.131 +val [prem1,prem2] = Goalw [Least_nat_def]
  10.132      "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
  10.133  by (rtac select_equality 1);
  10.134  by (blast_tac (claset() addSIs [prem1,prem2]) 1);
  10.135 @@ -513,8 +513,8 @@
  10.136  by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
  10.137  qed "Least_equality";
  10.138  
  10.139 -val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))";
  10.140 -by (rtac (prem RS rev_mp) 1);
  10.141 +Goal "P(k::nat) ==> P(LEAST x. P(x))";
  10.142 +by (etac rev_mp 1);
  10.143  by (res_inst_tac [("n","k")] less_induct 1);
  10.144  by (rtac impI 1);
  10.145  by (rtac classical 1);
  10.146 @@ -525,8 +525,8 @@
  10.147  qed "LeastI";
  10.148  
  10.149  (*Proof is almost identical to the one above!*)
  10.150 -val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k";
  10.151 -by (rtac (prem RS rev_mp) 1);
  10.152 +Goal "P(k::nat) ==> (LEAST x. P(x)) <= k";
  10.153 +by (etac rev_mp 1);
  10.154  by (res_inst_tac [("n","k")] less_induct 1);
  10.155  by (rtac impI 1);
  10.156  by (rtac classical 1);
  10.157 @@ -536,10 +536,9 @@
  10.158  by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1);
  10.159  qed "Least_le";
  10.160  
  10.161 -val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)";
  10.162 +Goal "k < (LEAST x. P(x)) ==> ~P(k::nat)";
  10.163  by (rtac notI 1);
  10.164 -by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
  10.165 -by (rtac prem 1);
  10.166 +by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
  10.167  qed "not_less_Least";
  10.168  
  10.169  (*** Instantiation of transitivity prover ***)
    11.1 --- a/src/HOL/Ord.ML	Thu Aug 13 18:07:56 1998 +0200
    11.2 +++ b/src/HOL/Ord.ML	Thu Aug 13 18:14:26 1998 +0200
    11.3 @@ -8,15 +8,13 @@
    11.4  
    11.5  (** mono **)
    11.6  
    11.7 -val [prem] = goalw Ord.thy [mono_def]
    11.8 +val [prem] = Goalw [mono_def]
    11.9      "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
   11.10  by (REPEAT (ares_tac [allI, impI, prem] 1));
   11.11  qed "monoI";
   11.12  
   11.13 -val [major,minor] = goalw Ord.thy [mono_def]
   11.14 -    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
   11.15 -by (rtac (major RS spec RS spec RS mp) 1);
   11.16 -by (rtac minor 1);
   11.17 +Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
   11.18 +by (Fast_tac 1);
   11.19  qed "monoD";
   11.20  
   11.21  
   11.22 @@ -46,7 +44,7 @@
   11.23  by (simp_tac (simpset() addsimps prems) 1);
   11.24  qed "min_leastL";
   11.25  
   11.26 -val prems = goalw thy [min_def]
   11.27 +val prems = Goalw [min_def]
   11.28   "(!!x::'a::order. least <= x) ==> min x least = least";
   11.29  by (cut_facts_tac prems 1);
   11.30  by (Asm_simp_tac 1);
    12.1 --- a/src/HOL/Prod.ML	Thu Aug 13 18:07:56 1998 +0200
    12.2 +++ b/src/HOL/Prod.ML	Thu Aug 13 18:14:26 1998 +0200
    12.3 @@ -24,7 +24,7 @@
    12.4  by (etac Abs_Prod_inverse 1);
    12.5  qed "inj_on_Abs_Prod";
    12.6  
    12.7 -val prems = goalw Prod.thy [Pair_def]
    12.8 +val prems = Goalw [Pair_def]
    12.9      "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
   12.10  by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
   12.11  by (REPEAT (ares_tac (prems@[ProdI]) 1));
   12.12 @@ -49,7 +49,7 @@
   12.13             rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
   12.14  qed "PairE_lemma";
   12.15  
   12.16 -val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
   12.17 +val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
   12.18  by (rtac (PairE_lemma RS exE) 1);
   12.19  by (REPEAT (eresolve_tac [prem,exE] 1));
   12.20  qed "PairE";
   12.21 @@ -222,7 +222,7 @@
   12.22  by (Asm_simp_tac 1);
   12.23  qed "splitI";
   12.24  
   12.25 -val prems = goalw Prod.thy [split_def]
   12.26 +val prems = Goalw [split_def]
   12.27      "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   12.28  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   12.29  qed "splitE";
   12.30 @@ -246,7 +246,7 @@
   12.31  by (Asm_simp_tac 1);
   12.32  qed "mem_splitI2";
   12.33  
   12.34 -val prems = goalw Prod.thy [split_def]
   12.35 +val prems = Goalw [split_def]
   12.36      "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   12.37  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   12.38  qed "mem_splitE";
   12.39 @@ -298,13 +298,13 @@
   12.40  qed "prod_fun_ident";
   12.41  Addsimps [prod_fun_ident];
   12.42  
   12.43 -val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
   12.44 +Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
   12.45  by (rtac image_eqI 1);
   12.46  by (rtac (prod_fun RS sym) 1);
   12.47 -by (resolve_tac prems 1);
   12.48 +by (assume_tac 1);
   12.49  qed "prod_fun_imageI";
   12.50  
   12.51 -val major::prems = goal Prod.thy
   12.52 +val major::prems = Goal
   12.53      "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   12.54  \    |] ==> P";
   12.55  by (rtac (major RS imageE) 1);
   12.56 @@ -354,7 +354,7 @@
   12.57  
   12.58  AddSEs [SigmaE2, SigmaE];
   12.59  
   12.60 -val prems = goal Prod.thy
   12.61 +val prems = Goal
   12.62      "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
   12.63  by (cut_facts_tac prems 1);
   12.64  by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   12.65 @@ -384,14 +384,14 @@
   12.66  
   12.67  (*** Domain of a relation ***)
   12.68  
   12.69 -val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
   12.70 +Goalw [image_def] "(a,b) : r ==> a : fst``r";
   12.71  by (rtac CollectI 1);
   12.72  by (rtac bexI 1);
   12.73  by (rtac (fst_conv RS sym) 1);
   12.74 -by (resolve_tac prems 1);
   12.75 +by (assume_tac 1);
   12.76  qed "fst_imageI";
   12.77  
   12.78 -val major::prems = goal Prod.thy
   12.79 +val major::prems = Goal
   12.80      "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
   12.81  by (rtac (major RS imageE) 1);
   12.82  by (resolve_tac prems 1);
   12.83 @@ -402,15 +402,14 @@
   12.84  
   12.85  (*** Range of a relation ***)
   12.86  
   12.87 -val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
   12.88 +Goalw [image_def] "(a,b) : r ==> b : snd``r";
   12.89  by (rtac CollectI 1);
   12.90  by (rtac bexI 1);
   12.91  by (rtac (snd_conv RS sym) 1);
   12.92 -by (resolve_tac prems 1);
   12.93 +by (assume_tac 1);
   12.94  qed "snd_imageI";
   12.95  
   12.96 -val major::prems = goal Prod.thy
   12.97 -    "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
   12.98 +val major::prems = Goal "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
   12.99  by (rtac (major RS imageE) 1);
  12.100  by (resolve_tac prems 1);
  12.101  by (etac ssubst 1);
    13.1 --- a/src/HOL/RelPow.ML	Thu Aug 13 18:07:56 1998 +0200
    13.2 +++ b/src/HOL/RelPow.ML	Thu Aug 13 18:14:26 1998 +0200
    13.3 @@ -31,14 +31,14 @@
    13.4  by (Asm_full_simp_tac 1);
    13.5  qed "rel_pow_0_E";
    13.6  
    13.7 -val [major,minor] = goal RelPow.thy
    13.8 +val [major,minor] = Goal
    13.9    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
   13.10  by (cut_facts_tac [major] 1);
   13.11  by (Asm_full_simp_tac  1);
   13.12  by (blast_tac (claset() addIs [minor]) 1);
   13.13  qed "rel_pow_Suc_E";
   13.14  
   13.15 -val [p1,p2,p3] = goal RelPow.thy
   13.16 +val [p1,p2,p3] = Goal
   13.17      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
   13.18  \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
   13.19  \    |] ==> P";
   13.20 @@ -52,18 +52,20 @@
   13.21  
   13.22  Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
   13.23  by (nat_ind_tac "n" 1);
   13.24 -by (blast_tac (claset() addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
   13.25 -by (blast_tac (claset() addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
   13.26 +by (blast_tac (claset() addIs [rel_pow_0_I] 
   13.27 +	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
   13.28 +by (blast_tac (claset() addIs [rel_pow_Suc_I]  
   13.29 +	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
   13.30  qed_spec_mp "rel_pow_Suc_D2";
   13.31  
   13.32  
   13.33  Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
   13.34  by (nat_ind_tac "n" 1);
   13.35 -by (fast_tac (claset() addss (simpset())) 1);
   13.36 -by (fast_tac (claset() addss (simpset())) 1);
   13.37 +by (ALLGOALS Asm_simp_tac);
   13.38 +by (Blast_tac 1);
   13.39  qed_spec_mp "rel_pow_Suc_D2'";
   13.40  
   13.41 -val [p1,p2,p3] = goal RelPow.thy
   13.42 +val [p1,p2,p3] = Goal
   13.43      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
   13.44  \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
   13.45  \    |] ==> P";
    14.1 --- a/src/HOL/Relation.ML	Thu Aug 13 18:07:56 1998 +0200
    14.2 +++ b/src/HOL/Relation.ML	Thu Aug 13 18:14:26 1998 +0200
    14.3 @@ -12,7 +12,7 @@
    14.4  by (Blast_tac 1);
    14.5  qed "idI";
    14.6  
    14.7 -val major::prems = goalw thy [id_def]
    14.8 +val major::prems = Goalw [id_def]
    14.9      "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
   14.10  \    |] ==>  P";  
   14.11  by (rtac (major RS CollectE) 1);
   14.12 @@ -34,7 +34,7 @@
   14.13  qed "compI";
   14.14  
   14.15  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
   14.16 -val prems = goalw thy [comp_def]
   14.17 +val prems = Goalw [comp_def]
   14.18      "[| xz : r O s;  \
   14.19  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
   14.20  \    |] ==> P";
   14.21 @@ -43,7 +43,7 @@
   14.22       ORELSE ares_tac prems 1));
   14.23  qed "compE";
   14.24  
   14.25 -val prems = goal thy
   14.26 +val prems = Goal
   14.27      "[| (a,c) : r O s;  \
   14.28  \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
   14.29  \    |] ==> P";
   14.30 @@ -78,7 +78,7 @@
   14.31  
   14.32  (** Natural deduction for trans(r) **)
   14.33  
   14.34 -val prems = goalw thy [trans_def]
   14.35 +val prems = Goalw [trans_def]
   14.36      "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
   14.37  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
   14.38  qed "transI";
    15.1 --- a/src/HOL/Set.ML	Thu Aug 13 18:07:56 1998 +0200
    15.2 +++ b/src/HOL/Set.ML	Thu Aug 13 18:14:26 1998 +0200
    15.3 @@ -17,17 +17,17 @@
    15.4  by (Asm_simp_tac 1);
    15.5  qed "CollectI";
    15.6  
    15.7 -val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
    15.8 +Goal "a : {x. P(x)} ==> P(a)";
    15.9  by (Asm_full_simp_tac 1);
   15.10  qed "CollectD";
   15.11  
   15.12 -val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B";
   15.13 +val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
   15.14  by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
   15.15  by (rtac Collect_mem_eq 1);
   15.16  by (rtac Collect_mem_eq 1);
   15.17  qed "set_ext";
   15.18  
   15.19 -val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
   15.20 +val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
   15.21  by (rtac (prem RS ext RS arg_cong) 1);
   15.22  qed "Collect_cong";
   15.23  
   15.24 @@ -39,17 +39,16 @@
   15.25  
   15.26  section "Bounded quantifiers";
   15.27  
   15.28 -val prems = goalw Set.thy [Ball_def]
   15.29 +val prems = Goalw [Ball_def]
   15.30      "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
   15.31  by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
   15.32  qed "ballI";
   15.33  
   15.34 -val [major,minor] = goalw Set.thy [Ball_def]
   15.35 -    "[| ! x:A. P(x);  x:A |] ==> P(x)";
   15.36 -by (rtac (minor RS (major RS spec RS mp)) 1);
   15.37 +Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
   15.38 +by (Blast_tac 1);
   15.39  qed "bspec";
   15.40  
   15.41 -val major::prems = goalw Set.thy [Ball_def]
   15.42 +val major::prems = Goalw [Ball_def]
   15.43      "[| ! x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
   15.44  by (rtac (major RS spec RS impCE) 1);
   15.45  by (REPEAT (eresolve_tac prems 1));
   15.46 @@ -61,9 +60,8 @@
   15.47  AddSIs [ballI];
   15.48  AddEs  [ballE];
   15.49  
   15.50 -val prems = goalw Set.thy [Bex_def]
   15.51 -    "[| P(x);  x:A |] ==> ? x:A. P(x)";
   15.52 -by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
   15.53 +Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
   15.54 +by (Blast_tac 1);
   15.55  qed "bexI";
   15.56  
   15.57  qed_goal "bexCI" Set.thy 
   15.58 @@ -72,7 +70,7 @@
   15.59    [ (rtac classical 1),
   15.60      (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
   15.61  
   15.62 -val major::prems = goalw Set.thy [Bex_def]
   15.63 +val major::prems = Goalw [Bex_def]
   15.64      "[| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
   15.65  by (rtac (major RS exE) 1);
   15.66  by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
   15.67 @@ -95,7 +93,7 @@
   15.68  
   15.69  (** Congruence rules **)
   15.70  
   15.71 -val prems = goal Set.thy
   15.72 +val prems = Goal
   15.73      "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
   15.74  \    (! x:A. P(x)) = (! x:B. Q(x))";
   15.75  by (resolve_tac (prems RL [ssubst]) 1);
   15.76 @@ -103,7 +101,7 @@
   15.77       ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
   15.78  qed "ball_cong";
   15.79  
   15.80 -val prems = goal Set.thy
   15.81 +val prems = Goal
   15.82      "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
   15.83  \    (? x:A. P(x)) = (? x:B. Q(x))";
   15.84  by (resolve_tac (prems RL [ssubst]) 1);
   15.85 @@ -113,7 +111,7 @@
   15.86  
   15.87  section "Subsets";
   15.88  
   15.89 -val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
   15.90 +val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
   15.91  by (REPEAT (ares_tac (prems @ [ballI]) 1));
   15.92  qed "subsetI";
   15.93  
   15.94 @@ -130,9 +128,8 @@
   15.95  Blast.overloaded ("op ``", domain_type o domain_type);
   15.96  
   15.97  (*Rule in Modus Ponens style*)
   15.98 -val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
   15.99 -by (rtac (major RS bspec) 1);
  15.100 -by (resolve_tac prems 1);
  15.101 +Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";
  15.102 +by (Blast_tac 1);
  15.103  qed "subsetD";
  15.104  
  15.105  (*The same, with reversed premises for use with etac -- cf rev_mp*)
  15.106 @@ -149,7 +146,7 @@
  15.107   (fn prems=>  [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
  15.108  
  15.109  (*Classical elimination rule*)
  15.110 -val major::prems = goalw Set.thy [subset_def] 
  15.111 +val major::prems = Goalw [subset_def] 
  15.112      "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
  15.113  by (rtac (major RS ballE) 1);
  15.114  by (REPEAT (eresolve_tac prems 1));
  15.115 @@ -164,7 +161,7 @@
  15.116  qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
  15.117   (fn _=> [Fast_tac 1]);		(*Blast_tac would try order_refl and fail*)
  15.118  
  15.119 -val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
  15.120 +Goal "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
  15.121  by (Blast_tac 1);
  15.122  qed "subset_trans";
  15.123  
  15.124 @@ -172,32 +169,32 @@
  15.125  section "Equality";
  15.126  
  15.127  (*Anti-symmetry of the subset relation*)
  15.128 -val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
  15.129 -by (rtac (iffI RS set_ext) 1);
  15.130 -by (REPEAT (ares_tac (prems RL [subsetD]) 1));
  15.131 +Goal "[| A <= B;  B <= A |] ==> A = (B::'a set)";
  15.132 +br set_ext 1;
  15.133 +by (blast_tac (claset() addIs [subsetD]) 1);
  15.134  qed "subset_antisym";
  15.135  val equalityI = subset_antisym;
  15.136  
  15.137  AddSIs [equalityI];
  15.138  
  15.139  (* Equality rules from ZF set theory -- are they appropriate here? *)
  15.140 -val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
  15.141 -by (resolve_tac (prems RL [subst]) 1);
  15.142 +Goal "A = B ==> A<=(B::'a set)";
  15.143 +by (etac ssubst 1);
  15.144  by (rtac subset_refl 1);
  15.145  qed "equalityD1";
  15.146  
  15.147 -val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
  15.148 -by (resolve_tac (prems RL [subst]) 1);
  15.149 +Goal "A = B ==> B<=(A::'a set)";
  15.150 +by (etac ssubst 1);
  15.151  by (rtac subset_refl 1);
  15.152  qed "equalityD2";
  15.153  
  15.154 -val prems = goal Set.thy
  15.155 +val prems = Goal
  15.156      "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
  15.157  by (resolve_tac prems 1);
  15.158  by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
  15.159  qed "equalityE";
  15.160  
  15.161 -val major::prems = goal Set.thy
  15.162 +val major::prems = Goal
  15.163      "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
  15.164  by (rtac (major RS equalityE) 1);
  15.165  by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
  15.166 @@ -206,7 +203,7 @@
  15.167  (*Lemma for creating induction formulae -- for "pattern matching" on p
  15.168    To make the induction hypotheses usable, apply "spec" or "bspec" to
  15.169    put universal quantifiers over the free variables in p. *)
  15.170 -val prems = goal Set.thy 
  15.171 +val prems = Goal 
  15.172      "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
  15.173  by (rtac mp 1);
  15.174  by (REPEAT (resolve_tac (refl::prems) 1));
  15.175 @@ -305,17 +302,15 @@
  15.176  
  15.177  Addsimps [Compl_iff];
  15.178  
  15.179 -val prems = goalw Set.thy [Compl_def]
  15.180 -    "[| c:A ==> False |] ==> c : Compl(A)";
  15.181 +val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)";
  15.182  by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
  15.183  qed "ComplI";
  15.184  
  15.185  (*This form, with negated conclusion, works well with the Classical prover.
  15.186    Negated assumptions behave like formulae on the right side of the notional
  15.187    turnstile...*)
  15.188 -val major::prems = goalw Set.thy [Compl_def]
  15.189 -    "c : Compl(A) ==> c~:A";
  15.190 -by (rtac (major RS CollectD) 1);
  15.191 +Goalw [Compl_def] "c : Compl(A) ==> c~:A";
  15.192 +by (etac CollectD 1);
  15.193  qed "ComplD";
  15.194  
  15.195  val ComplE = make_elim ComplD;
  15.196 @@ -345,7 +340,7 @@
  15.197    [ (Simp_tac 1),
  15.198      (REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
  15.199  
  15.200 -val major::prems = goalw Set.thy [Un_def]
  15.201 +val major::prems = Goalw [Un_def]
  15.202      "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
  15.203  by (rtac (major RS CollectD RS disjE) 1);
  15.204  by (REPEAT (eresolve_tac prems 1));
  15.205 @@ -374,7 +369,7 @@
  15.206  by (Asm_full_simp_tac 1);
  15.207  qed "IntD2";
  15.208  
  15.209 -val [major,minor] = goal Set.thy
  15.210 +val [major,minor] = Goal
  15.211      "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
  15.212  by (rtac minor 1);
  15.213  by (rtac (major RS IntD1) 1);
  15.214 @@ -479,7 +474,7 @@
  15.215  by Auto_tac;
  15.216  qed "UN_I";
  15.217  
  15.218 -val major::prems = goalw Set.thy [UNION_def]
  15.219 +val major::prems = Goalw [UNION_def]
  15.220      "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
  15.221  by (rtac (major RS CollectD RS bexE) 1);
  15.222  by (REPEAT (ares_tac prems 1));
  15.223 @@ -488,7 +483,7 @@
  15.224  AddIs  [UN_I];
  15.225  AddSEs [UN_E];
  15.226  
  15.227 -val prems = goal Set.thy
  15.228 +val prems = Goal
  15.229      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
  15.230  \    (UN x:A. C(x)) = (UN x:B. D(x))";
  15.231  by (REPEAT (etac UN_E 1
  15.232 @@ -505,7 +500,7 @@
  15.233  
  15.234  Addsimps [INT_iff];
  15.235  
  15.236 -val prems = goalw Set.thy [INTER_def]
  15.237 +val prems = Goalw [INTER_def]
  15.238      "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
  15.239  by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
  15.240  qed "INT_I";
  15.241 @@ -515,7 +510,7 @@
  15.242  qed "INT_D";
  15.243  
  15.244  (*"Classical" elimination -- by the Excluded Middle on a:A *)
  15.245 -val major::prems = goalw Set.thy [INTER_def]
  15.246 +val major::prems = Goalw [INTER_def]
  15.247      "[| b : (INT x:A. B(x));  b: B(a) ==> R;  a~:A ==> R |] ==> R";
  15.248  by (rtac (major RS CollectD RS ballE) 1);
  15.249  by (REPEAT (eresolve_tac prems 1));
  15.250 @@ -524,7 +519,7 @@
  15.251  AddSIs [INT_I];
  15.252  AddEs  [INT_D, INT_E];
  15.253  
  15.254 -val prems = goal Set.thy
  15.255 +val prems = Goal
  15.256      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
  15.257  \    (INT x:A. C(x)) = (INT x:B. D(x))";
  15.258  by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
  15.259 @@ -546,7 +541,7 @@
  15.260  by Auto_tac;
  15.261  qed "UnionI";
  15.262  
  15.263 -val major::prems = goalw Set.thy [Union_def]
  15.264 +val major::prems = Goalw [Union_def]
  15.265      "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
  15.266  by (rtac (major RS UN_E) 1);
  15.267  by (REPEAT (ares_tac prems 1));
  15.268 @@ -564,7 +559,7 @@
  15.269  
  15.270  Addsimps [Inter_iff];
  15.271  
  15.272 -val prems = goalw Set.thy [Inter_def]
  15.273 +val prems = Goalw [Inter_def]
  15.274      "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
  15.275  by (REPEAT (ares_tac ([INT_I] @ prems) 1));
  15.276  qed "InterI";
  15.277 @@ -576,7 +571,7 @@
  15.278  qed "InterD";
  15.279  
  15.280  (*"Classical" elimination rule -- does not require proving X:C *)
  15.281 -val major::prems = goalw Set.thy [Inter_def]
  15.282 +val major::prems = Goalw [Inter_def]
  15.283      "[| A : Inter(C);  X~:C ==> R;  A:X ==> R |] ==> R";
  15.284  by (rtac (major RS INT_E) 1);
  15.285  by (REPEAT (eresolve_tac prems 1));
  15.286 @@ -589,15 +584,15 @@
  15.287  (*** Image of a set under a function ***)
  15.288  
  15.289  (*Frequently b does not have the syntactic form of f(x).*)
  15.290 -val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
  15.291 -by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
  15.292 +Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
  15.293 +by (Blast_tac 1);
  15.294  qed "image_eqI";
  15.295  Addsimps [image_eqI];
  15.296  
  15.297  bind_thm ("imageI", refl RS image_eqI);
  15.298  
  15.299  (*The eta-expansion gives variable-name preservation.*)
  15.300 -val major::prems = goalw thy [image_def]
  15.301 +val major::prems = Goalw [image_def]
  15.302      "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
  15.303  by (rtac (major RS CollectD RS bexE) 1);
  15.304  by (REPEAT (ares_tac prems 1));
  15.305 @@ -621,7 +616,7 @@
  15.306  
  15.307  (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
  15.308    many existing proofs.*)
  15.309 -val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
  15.310 +val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
  15.311  by (blast_tac (claset() addIs prems) 1);
  15.312  qed "image_subsetI";
  15.313  
  15.314 @@ -634,7 +629,7 @@
  15.315  
  15.316  bind_thm ("rangeI", UNIV_I RS imageI);
  15.317  
  15.318 -val [major,minor] = goal thy 
  15.319 +val [major,minor] = Goal 
  15.320      "[| b : range(%x. f(x));  !!x. b=f(x) ==> P |] ==> P"; 
  15.321  by (rtac (major RS imageE) 1);
  15.322  by (etac minor 1);
    16.1 --- a/src/HOL/Sum.ML	Thu Aug 13 18:07:56 1998 +0200
    16.2 +++ b/src/HOL/Sum.ML	Thu Aug 13 18:14:26 1998 +0200
    16.3 @@ -3,7 +3,7 @@
    16.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.5      Copyright   1991  University of Cambridge
    16.6  
    16.7 -For Sum.thy.  The disjoint sum of two types
    16.8 +The disjoint sum of two types
    16.9  *)
   16.10  
   16.11  open Sum;
   16.12 @@ -51,13 +51,13 @@
   16.13  
   16.14  (** Injectiveness of Inl and Inr **)
   16.15  
   16.16 -val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
   16.17 -by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
   16.18 +Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
   16.19 +by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
   16.20  by (Blast_tac 1);
   16.21  qed "Inl_Rep_inject";
   16.22  
   16.23 -val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
   16.24 -by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
   16.25 +Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
   16.26 +by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
   16.27  by (Blast_tac 1);
   16.28  qed "Inr_Rep_inject";
   16.29  
   16.30 @@ -101,7 +101,7 @@
   16.31  
   16.32  (** Elimination rules **)
   16.33  
   16.34 -val major::prems = goalw Sum.thy [sum_def]
   16.35 +val major::prems = Goalw [sum_def]
   16.36      "[| u: A Plus B;  \
   16.37  \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
   16.38  \       !!y. [| y:B;  u=Inr(y) |] ==> P \
   16.39 @@ -130,7 +130,7 @@
   16.40  
   16.41  (** Exhaustion rule for sums -- a degenerate form of induction **)
   16.42  
   16.43 -val prems = goalw Sum.thy [Inl_def,Inr_def]
   16.44 +val prems = Goalw [Inl_def,Inr_def]
   16.45      "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
   16.46  \    |] ==> P";
   16.47  by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
   16.48 @@ -140,7 +140,7 @@
   16.49                      rtac (Rep_Sum_inverse RS sym)]));
   16.50  qed "sumE";
   16.51  
   16.52 -val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
   16.53 +val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
   16.54  by (res_inst_tac [("s","x")] sumE 1);
   16.55  by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
   16.56  qed "sum_induct";
   16.57 @@ -177,7 +177,7 @@
   16.58  
   16.59  val PartI = refl RSN (2,Part_eqI);
   16.60  
   16.61 -val major::prems = goalw Sum.thy [Part_def]
   16.62 +val major::prems = Goalw [Part_def]
   16.63      "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
   16.64  \    |] ==> P";
   16.65  by (rtac (major RS IntE) 1);
    17.1 --- a/src/HOL/Trancl.ML	Thu Aug 13 18:07:56 1998 +0200
    17.2 +++ b/src/HOL/Trancl.ML	Thu Aug 13 18:14:26 1998 +0200
    17.3 @@ -3,7 +3,7 @@
    17.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.5      Copyright   1992  University of Cambridge
    17.6  
    17.7 -For Trancl.thy.  Theorems about the transitive closure of a relation
    17.8 +Theorems about the transitive closure of a relation
    17.9  *)
   17.10  
   17.11  open Trancl;
   17.12 @@ -46,7 +46,7 @@
   17.13  
   17.14  (** standard induction rule **)
   17.15  
   17.16 -val major::prems = goal Trancl.thy 
   17.17 +val major::prems = Goal 
   17.18    "[| (a,b) : r^*; \
   17.19  \     !!x. P((x,x)); \
   17.20  \     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
   17.21 @@ -56,7 +56,7 @@
   17.22  qed "rtrancl_full_induct";
   17.23  
   17.24  (*nice induction rule*)
   17.25 -val major::prems = goal Trancl.thy
   17.26 +val major::prems = Goal
   17.27      "[| (a::'a,b) : r^*;    \
   17.28  \       P(a); \
   17.29  \       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
   17.30 @@ -85,7 +85,7 @@
   17.31  
   17.32  
   17.33  (*elimination of rtrancl -- by induction on a special formula*)
   17.34 -val major::prems = goal Trancl.thy
   17.35 +val major::prems = Goal
   17.36      "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
   17.37  \       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
   17.38  \    |] ==> P";
   17.39 @@ -133,8 +133,9 @@
   17.40  qed "rtrancl_subset";
   17.41  
   17.42  Goal "(R^* Un S^*)^* = (R Un S)^*";
   17.43 -by (blast_tac (claset() addSIs [rtrancl_subset]
   17.44 -                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
   17.45 +(*Blast_tac: PROOF FAILED*)
   17.46 +by (Blast.depth_tac (claset() addSIs [rtrancl_subset]
   17.47 +                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 4 1);
   17.48  qed "rtrancl_Un_rtrancl";
   17.49  
   17.50  Goal "(R^=)^* = R^*";
   17.51 @@ -160,7 +161,7 @@
   17.52  by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
   17.53  qed "rtrancl_converse";
   17.54  
   17.55 -val major::prems = goal Trancl.thy
   17.56 +val major::prems = Goal
   17.57      "[| (a,b) : r^*; P(b); \
   17.58  \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
   17.59  \     ==> P(a)";
   17.60 @@ -169,7 +170,7 @@
   17.61  by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
   17.62  qed "converse_rtrancl_induct";
   17.63  
   17.64 -val prems = goal Trancl.thy
   17.65 +val prems = Goal
   17.66   "[| ((a,b),(c,d)) : r^*; P c d; \
   17.67  \    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
   17.68  \ |] ==> P a b";
   17.69 @@ -183,7 +184,7 @@
   17.70  by (REPEAT(ares_tac prems 1));
   17.71  qed "converse_rtrancl_induct2";
   17.72  
   17.73 -val major::prems = goal Trancl.thy
   17.74 +val major::prems = Goal
   17.75   "[| (x,z):r^*; \
   17.76  \    x=z ==> P; \
   17.77  \    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
   17.78 @@ -237,7 +238,7 @@
   17.79  qed "rtrancl_into_trancl2";
   17.80  
   17.81  (*Nice induction rule for trancl*)
   17.82 -val major::prems = goal Trancl.thy
   17.83 +val major::prems = Goal
   17.84    "[| (a,b) : r^+;                                      \
   17.85  \     !!y.  [| (a,y) : r |] ==> P(y);                   \
   17.86  \     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
   17.87 @@ -252,7 +253,7 @@
   17.88  qed "trancl_induct";
   17.89  
   17.90  (*elimination of r^+ -- NOT an induction rule*)
   17.91 -val major::prems = goal Trancl.thy
   17.92 +val major::prems = Goal
   17.93      "[| (a::'a,b) : r^+;  \
   17.94  \       (a,b) : r ==> P; \
   17.95  \       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
    18.1 --- a/src/HOL/Univ.ML	Thu Aug 13 18:07:56 1998 +0200
    18.2 +++ b/src/HOL/Univ.ML	Thu Aug 13 18:14:26 1998 +0200
    18.3 @@ -14,7 +14,7 @@
    18.4  by (rtac split 1);
    18.5  qed "apfst_conv";
    18.6  
    18.7 -val [major,minor] = goal Univ.thy
    18.8 +val [major,minor] = Goal
    18.9      "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
   18.10  \    |] ==> R";
   18.11  by (rtac PairE 1);
   18.12 @@ -27,26 +27,27 @@
   18.13  
   18.14  (** Push -- an injection, analogous to Cons on lists **)
   18.15  
   18.16 -val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> i=j";
   18.17 -by (rtac (major RS fun_cong RS box_equals RS Suc_inject) 1);
   18.18 +Goalw [Push_def] "Push i f = Push j g  ==> i=j";
   18.19 +by (etac (fun_cong RS box_equals RS Suc_inject) 1);
   18.20  by (rtac nat_case_0 1);
   18.21  by (rtac nat_case_0 1);
   18.22  qed "Push_inject1";
   18.23  
   18.24 -val [major] = goalw Univ.thy [Push_def] "Push i f = Push j g  ==> f=g";
   18.25 -by (rtac (major RS fun_cong RS ext RS box_equals) 1);
   18.26 +Goalw [Push_def] "Push i f = Push j g  ==> f=g";
   18.27 +by (rtac (ext RS box_equals) 1);
   18.28 +by (etac fun_cong 1);
   18.29  by (rtac (nat_case_Suc RS ext) 1);
   18.30  by (rtac (nat_case_Suc RS ext) 1);
   18.31  qed "Push_inject2";
   18.32  
   18.33 -val [major,minor] = goal Univ.thy
   18.34 +val [major,minor] = Goal
   18.35      "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P \
   18.36  \    |] ==> P";
   18.37  by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
   18.38  qed "Push_inject";
   18.39  
   18.40 -val [major] = goalw Univ.thy [Push_def] "Push k f =(%z.0) ==> P";
   18.41 -by (rtac (major RS fun_cong RS box_equals RS Suc_neq_Zero) 1);
   18.42 +Goalw [Push_def] "Push k f =(%z.0) ==> P";
   18.43 +by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1);
   18.44  by (rtac nat_case_0 1);
   18.45  by (rtac refl 1);
   18.46  qed "Push_neq_K0";
   18.47 @@ -125,7 +126,7 @@
   18.48  
   18.49  (** Injectiveness of Push_Node **)
   18.50  
   18.51 -val [major,minor] = goalw Univ.thy [Push_Node_def]
   18.52 +val [major,minor] = Goalw [Push_Node_def]
   18.53      "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
   18.54  \    |] ==> P";
   18.55  by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
   18.56 @@ -150,17 +151,17 @@
   18.57  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
   18.58  qed "Scons_inject_lemma2";
   18.59  
   18.60 -val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> M=M'";
   18.61 -by (rtac (major RS equalityE) 1);
   18.62 +Goal "Scons M N = Scons M' N' ==> M=M'";
   18.63 +by (etac equalityE 1);
   18.64  by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
   18.65  qed "Scons_inject1";
   18.66  
   18.67 -val [major] = goal Univ.thy "Scons M N = Scons M' N' ==> N=N'";
   18.68 -by (rtac (major RS equalityE) 1);
   18.69 +Goal "Scons M N = Scons M' N' ==> N=N'";
   18.70 +by (etac equalityE 1);
   18.71  by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
   18.72  qed "Scons_inject2";
   18.73  
   18.74 -val [major,minor] = goal Univ.thy
   18.75 +val [major,minor] = Goal
   18.76      "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P \
   18.77  \    |] ==> P";
   18.78  by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
   18.79 @@ -302,7 +303,7 @@
   18.80  qed "uprodI";
   18.81  
   18.82  (*The general elimination rule*)
   18.83 -val major::prems = goalw Univ.thy [uprod_def]
   18.84 +val major::prems = Goalw [uprod_def]
   18.85      "[| c : A<*>B;  \
   18.86  \       !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P \
   18.87  \    |] ==> P";
   18.88 @@ -312,7 +313,7 @@
   18.89  qed "uprodE";
   18.90  
   18.91  (*Elimination of a pair -- introduces no eigenvariables*)
   18.92 -val prems = goal Univ.thy
   18.93 +val prems = Goal
   18.94      "[| Scons M N : A<*>B;      [| M:A;  N:B |] ==> P   \
   18.95  \    |] ==> P";
   18.96  by (rtac uprodE 1);
   18.97 @@ -330,7 +331,7 @@
   18.98  by (Blast_tac 1);
   18.99  qed "usum_In1I";
  18.100  
  18.101 -val major::prems = goalw Univ.thy [usum_def]
  18.102 +val major::prems = Goalw [usum_def]
  18.103      "[| u : A<+>B;  \
  18.104  \       !!x. [| x:A;  u=In0(x) |] ==> P; \
  18.105  \       !!y. [| y:B;  u=In1(y) |] ==> P \
  18.106 @@ -352,12 +353,12 @@
  18.107  
  18.108  AddIffs [In0_not_In1, In1_not_In0];
  18.109  
  18.110 -val [major] = goalw Univ.thy [In0_def] "In0(M) = In0(N) ==>  M=N";
  18.111 -by (rtac (major RS Scons_inject2) 1);
  18.112 +Goalw [In0_def] "In0(M) = In0(N) ==>  M=N";
  18.113 +by (etac (Scons_inject2) 1);
  18.114  qed "In0_inject";
  18.115  
  18.116 -val [major] = goalw Univ.thy [In1_def] "In1(M) = In1(N) ==>  M=N";
  18.117 -by (rtac (major RS Scons_inject2) 1);
  18.118 +Goalw [In1_def] "In1(M) = In1(N) ==>  M=N";
  18.119 +by (etac (Scons_inject2) 1);
  18.120  qed "In1_inject";
  18.121  
  18.122  Goal "(In0 M = In0 N) = (M=N)";
  18.123 @@ -385,14 +386,13 @@
  18.124  by (Blast_tac 1);
  18.125  qed "ntrunc_subsetI";
  18.126  
  18.127 -val [major] = goalw Univ.thy [ntrunc_def]
  18.128 -    "(!!k. ntrunc k M <= N) ==> M<=N";
  18.129 +val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
  18.130  by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
  18.131  			       major RS subsetD]) 1);
  18.132  qed "ntrunc_subsetD";
  18.133  
  18.134  (*A generalized form of the take-lemma*)
  18.135 -val [major] = goal Univ.thy "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
  18.136 +val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
  18.137  by (rtac equalityI 1);
  18.138  by (ALLGOALS (rtac ntrunc_subsetD));
  18.139  by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
  18.140 @@ -400,7 +400,7 @@
  18.141  by (rtac (major RS equalityD2) 1);
  18.142  qed "ntrunc_equality";
  18.143  
  18.144 -val [major] = goalw Univ.thy [o_def]
  18.145 +val [major] = Goalw [o_def]
  18.146      "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
  18.147  by (rtac (ntrunc_equality RS ext) 1);
  18.148  by (rtac (major RS fun_cong) 1);
  18.149 @@ -478,7 +478,7 @@
  18.150  val diagI = refl RS diag_eqI |> standard;
  18.151  
  18.152  (*The general elimination rule*)
  18.153 -val major::prems = goalw Univ.thy [diag_def]
  18.154 +val major::prems = Goalw [diag_def]
  18.155      "[| c : diag(A);  \
  18.156  \       !!x y. [| x:A;  c = (x,x) |] ==> P \
  18.157  \    |] ==> P";
  18.158 @@ -494,7 +494,7 @@
  18.159  qed "dprodI";
  18.160  
  18.161  (*The general elimination rule*)
  18.162 -val major::prems = goalw Univ.thy [dprod_def]
  18.163 +val major::prems = Goalw [dprod_def]
  18.164      "[| c : r<**>s;  \
  18.165  \       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (Scons x y, Scons x' y') |] ==> P \
  18.166  \    |] ==> P";
  18.167 @@ -514,7 +514,7 @@
  18.168  by (Blast_tac 1);
  18.169  qed "dsum_In1I";
  18.170  
  18.171 -val major::prems = goalw Univ.thy [dsum_def]
  18.172 +val major::prems = Goalw [dsum_def]
  18.173      "[| w : r<++>s;  \
  18.174  \       !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P; \
  18.175  \       !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P \
    19.1 --- a/src/HOL/WF.ML	Thu Aug 13 18:07:56 1998 +0200
    19.2 +++ b/src/HOL/WF.ML	Thu Aug 13 18:14:26 1998 +0200
    19.3 @@ -12,7 +12,7 @@
    19.4  val H_cong1 = refl RS H_cong;
    19.5  
    19.6  (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
    19.7 -val [prem1,prem2] = goalw WF.thy [wf_def]
    19.8 +val [prem1,prem2] = Goalw [wf_def]
    19.9   "[| r <= A Times A;  \
   19.10  \    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
   19.11  \ ==>  wf(r)";
   19.12 @@ -22,7 +22,7 @@
   19.13  by (best_tac (claset() addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
   19.14  qed "wfI";
   19.15  
   19.16 -val major::prems = goalw WF.thy [wf_def]
   19.17 +val major::prems = Goalw [wf_def]
   19.18      "[| wf(r);          \
   19.19  \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
   19.20  \    |]  ==>  P(a)";
   19.21 @@ -36,26 +36,25 @@
   19.22             rename_last_tac a ["1"] (i+1),
   19.23             ares_tac prems i];
   19.24  
   19.25 -val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
   19.26 +Goal "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
   19.27  by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
   19.28 -by (blast_tac (claset() addIs prems) 1);
   19.29 -by (wf_ind_tac "a" prems 1);
   19.30 +by (Blast_tac 1);
   19.31 +by (wf_ind_tac "a" [] 1);
   19.32  by (Blast_tac 1);
   19.33  qed "wf_asym";
   19.34  
   19.35 -val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
   19.36 -by (rtac wf_asym 1);
   19.37 -by (REPEAT (resolve_tac prems 1));
   19.38 +Goal "[| wf(r);  (a,a): r |] ==> P";
   19.39 +by (blast_tac (claset() addEs [wf_asym]) 1);
   19.40  qed "wf_irrefl";
   19.41  
   19.42  (*transitive closure of a wf relation is wf! *)
   19.43 -val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
   19.44 -by (rewtac wf_def);
   19.45 +Goal "wf(r) ==> wf(r^+)";
   19.46 +by (stac wf_def 1);
   19.47  by (Clarify_tac 1);
   19.48  (*must retain the universal formula for later use!*)
   19.49  by (rtac allE 1 THEN assume_tac 1);
   19.50  by (etac mp 1);
   19.51 -by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
   19.52 +by (eres_inst_tac [("a","x")] wf_induct 1);
   19.53  by (rtac (impI RS allI) 1);
   19.54  by (etac tranclE 1);
   19.55  by (Blast_tac 1);
   19.56 @@ -72,14 +71,13 @@
   19.57   * Minimal-element characterization of well-foundedness
   19.58   *---------------------------------------------------------------------------*)
   19.59  
   19.60 -val wfr::_ = goalw WF.thy [wf_def]
   19.61 -    "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
   19.62 -by (rtac (wfr RS spec RS mp RS spec) 1);
   19.63 +Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
   19.64 +bd spec 1;
   19.65 +by (etac (mp RS spec) 1);
   19.66  by (Blast_tac 1);
   19.67  val lemma1 = result();
   19.68  
   19.69 -Goalw [wf_def]
   19.70 -    "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
   19.71 +Goalw [wf_def] "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
   19.72  by (Clarify_tac 1);
   19.73  by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
   19.74  by (Blast_tac 1);
   19.75 @@ -138,11 +136,10 @@
   19.76   * Wellfoundedness of `disjoint union'
   19.77   *---------------------------------------------------------------------------*)
   19.78  
   19.79 -Goal
   19.80 - "[| !i:I. wf(r i); \
   19.81 -\    !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
   19.82 -\                              Domain(r j) Int Range(r i) = {} \
   19.83 -\ |] ==> wf(UN i:I. r i)";
   19.84 +Goal "[| !i:I. wf(r i); \
   19.85 +\        !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
   19.86 +\                                  Domain(r j) Int Range(r i) = {} \
   19.87 +\     |] ==> wf(UN i:I. r i)";
   19.88  by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
   19.89  by(Clarify_tac 1);
   19.90  by(rename_tac "A a" 1);
   19.91 @@ -181,9 +178,8 @@
   19.92  by(Blast_tac 1);
   19.93  qed "wf_Union";
   19.94  
   19.95 -Goal
   19.96 - "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
   19.97 -\ |] ==> wf(r Un s)";
   19.98 +Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
   19.99 +\     |] ==> wf(r Un s)";
  19.100  br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
  19.101  by(Blast_tac 1);
  19.102  by(Blast_tac 1);
  19.103 @@ -251,10 +247,9 @@
  19.104                          eresolve_tac [transD, mp, allE]));
  19.105  val wf_super_ss = HOL_ss addSolver indhyp_tac;
  19.106  
  19.107 -val prems = goalw WF.thy [is_recfun_def,cut_def]
  19.108 +Goalw [is_recfun_def,cut_def]
  19.109      "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
  19.110      \ (x,a):r --> (x,b):r --> f(x)=g(x)";
  19.111 -by (cut_facts_tac prems 1);
  19.112  by (etac wf_induct 1);
  19.113  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
  19.114  by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
  19.115 @@ -274,15 +269,13 @@
  19.116  
  19.117  (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
  19.118  
  19.119 -val prems = goalw WF.thy [the_recfun_def]
  19.120 +Goalw [the_recfun_def]
  19.121      "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
  19.122 -by (res_inst_tac [("P", "is_recfun r H a")] selectI 1);
  19.123 -by (resolve_tac prems 1);
  19.124 +by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1);
  19.125  qed "is_the_recfun";
  19.126  
  19.127 -val prems = goal WF.thy
  19.128 - "!!r. [| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
  19.129 -by (wf_ind_tac "a" prems 1);
  19.130 +Goal "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
  19.131 +by (wf_ind_tac "a" [] 1);
  19.132  by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
  19.133                   is_the_recfun 1);
  19.134  by (rewtac is_recfun_def);
  19.135 @@ -309,7 +302,7 @@
  19.136  val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;
  19.137  
  19.138  (*--------------Old proof-----------------------------------------------------
  19.139 -val prems = goal WF.thy
  19.140 +val prems = Goal
  19.141      "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
  19.142  by (cut_facts_tac prems 1);
  19.143  by (wf_ind_tac "a" prems 1);
  19.144 @@ -376,7 +369,7 @@
  19.145  (*---------------------------------------------------------------------------
  19.146   * This form avoids giant explosions in proofs.  NOTE USE OF == 
  19.147   *---------------------------------------------------------------------------*)
  19.148 -val rew::prems = goal WF.thy
  19.149 +val rew::prems = goal thy
  19.150      "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
  19.151  by (rewtac rew);
  19.152  by (REPEAT (resolve_tac (prems@[wfrec]) 1));
    20.1 --- a/src/HOL/arith_data.ML	Thu Aug 13 18:07:56 1998 +0200
    20.2 +++ b/src/HOL/arith_data.ML	Thu Aug 13 18:14:26 1998 +0200
    20.3 @@ -56,7 +56,7 @@
    20.4  val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    20.5  
    20.6  fun prove_conv expand_tac norm_tac sg (t, u) =
    20.7 -  meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
    20.8 +  meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
    20.9      (K [expand_tac, norm_tac]))
   20.10    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   20.11      (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
    21.1 --- a/src/HOL/equalities.ML	Thu Aug 13 18:07:56 1998 +0200
    21.2 +++ b/src/HOL/equalities.ML	Thu Aug 13 18:14:26 1998 +0200
    21.3 @@ -136,7 +136,7 @@
    21.4  qed "if_image_distrib";
    21.5  Addsimps[if_image_distrib];
    21.6  
    21.7 -val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
    21.8 +val prems= Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
    21.9  by (rtac set_ext 1);
   21.10  by (simp_tac (simpset() addsimps image_def::prems) 1);
   21.11  qed "image_cong";
   21.12 @@ -212,10 +212,6 @@
   21.13  by (Blast_tac 1);
   21.14  qed "Int_Un_distrib2";
   21.15  
   21.16 -Goal "(A<=B) = (A Int B = A)";
   21.17 -by (blast_tac (claset() addSEs [equalityCE]) 1);
   21.18 -qed "subset_Int_eq";
   21.19 -
   21.20  Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
   21.21  by (blast_tac (claset() addEs [equalityCE]) 1);
   21.22  qed "Int_UNIV";
    22.1 --- a/src/HOL/mono.ML	Thu Aug 13 18:07:56 1998 +0200
    22.2 +++ b/src/HOL/mono.ML	Thu Aug 13 18:14:26 1998 +0200
    22.3 @@ -6,96 +6,96 @@
    22.4  Monotonicity of various operations
    22.5  *)
    22.6  
    22.7 -goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
    22.8 +Goal "A<=B ==> f``A <= f``B";
    22.9  by (Blast_tac 1);
   22.10  qed "image_mono";
   22.11  
   22.12 -goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
   22.13 +Goal "A<=B ==> Pow(A) <= Pow(B)";
   22.14  by (Blast_tac 1);
   22.15  qed "Pow_mono";
   22.16  
   22.17 -goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
   22.18 +Goal "A<=B ==> Union(A) <= Union(B)";
   22.19  by (Blast_tac 1);
   22.20  qed "Union_mono";
   22.21  
   22.22 -goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
   22.23 +Goal "B<=A ==> Inter(A) <= Inter(B)";
   22.24  by (Blast_tac 1);
   22.25  qed "Inter_anti_mono";
   22.26  
   22.27 -val prems = goal Set.thy
   22.28 +val prems = Goal
   22.29      "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   22.30  \    (UN x:A. f(x)) <= (UN x:B. g(x))";
   22.31  by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   22.32  qed "UN_mono";
   22.33  
   22.34  (*The last inclusion is POSITIVE! *)
   22.35 -val prems = goal Set.thy
   22.36 +val prems = Goal
   22.37      "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   22.38  \    (INT x:A. f(x)) <= (INT x:A. g(x))";
   22.39  by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   22.40  qed "INT_anti_mono";
   22.41  
   22.42 -goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
   22.43 +Goal "C<=D ==> insert a C <= insert a D";
   22.44  by (Blast_tac 1);
   22.45  qed "insert_mono";
   22.46  
   22.47 -goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
   22.48 +Goal "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
   22.49  by (Blast_tac 1);
   22.50  qed "Un_mono";
   22.51  
   22.52 -goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
   22.53 +Goal "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
   22.54  by (Blast_tac 1);
   22.55  qed "Int_mono";
   22.56  
   22.57 -goal Set.thy "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
   22.58 +Goal "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
   22.59  by (Blast_tac 1);
   22.60  qed "Diff_mono";
   22.61  
   22.62 -goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
   22.63 +Goal "A<=B ==> Compl(B) <= Compl(A)";
   22.64  by (Blast_tac 1);
   22.65  qed "Compl_anti_mono";
   22.66  
   22.67  (** Monotonicity of implications.  For inductive definitions **)
   22.68  
   22.69 -goal Set.thy "!!A B x. A<=B ==> x:A --> x:B";
   22.70 +Goal "A<=B ==> x:A --> x:B";
   22.71  by (rtac impI 1);
   22.72  by (etac subsetD 1);
   22.73  by (assume_tac 1);
   22.74  qed "in_mono";
   22.75  
   22.76 -goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
   22.77 +Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
   22.78  by (Blast_tac 1);
   22.79  qed "conj_mono";
   22.80  
   22.81 -goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
   22.82 +Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
   22.83  by (Blast_tac 1);
   22.84  qed "disj_mono";
   22.85  
   22.86 -goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
   22.87 +Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
   22.88  by (Blast_tac 1);
   22.89  qed "imp_mono";
   22.90  
   22.91 -goal HOL.thy "P-->P";
   22.92 +Goal "P-->P";
   22.93  by (rtac impI 1);
   22.94  by (assume_tac 1);
   22.95  qed "imp_refl";
   22.96  
   22.97 -val [PQimp] = goal HOL.thy
   22.98 +val [PQimp] = Goal
   22.99      "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
  22.100  by (blast_tac (claset() addIs [PQimp RS mp]) 1);
  22.101  qed "ex_mono";
  22.102  
  22.103 -val [PQimp] = goal HOL.thy
  22.104 +val [PQimp] = Goal
  22.105      "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
  22.106  by (blast_tac (claset() addIs [PQimp RS mp]) 1);
  22.107  qed "all_mono";
  22.108  
  22.109 -val [PQimp] = goal Set.thy
  22.110 +val [PQimp] = Goal
  22.111      "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
  22.112  by (blast_tac (claset() addIs [PQimp RS mp]) 1);
  22.113  qed "Collect_mono";
  22.114  
  22.115 -val [subs,PQimp] = goal Set.thy
  22.116 +val [subs,PQimp] = Goal
  22.117      "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
  22.118  \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
  22.119  by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
    23.1 --- a/src/HOL/subset.ML	Thu Aug 13 18:07:56 1998 +0200
    23.2 +++ b/src/HOL/subset.ML	Thu Aug 13 18:14:26 1998 +0200
    23.3 @@ -12,32 +12,28 @@
    23.4  qed_goal "subset_insertI" Set.thy "B <= insert a B"
    23.5   (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
    23.6  
    23.7 -goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
    23.8 +Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
    23.9  by (Blast_tac 1);
   23.10  qed "subset_insert";
   23.11  
   23.12  (*** Big Union -- least upper bound of a set  ***)
   23.13  
   23.14 -val prems = goal Set.thy
   23.15 -    "B:A ==> B <= Union(A)";
   23.16 -by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
   23.17 +Goal "B:A ==> B <= Union(A)";
   23.18 +by (REPEAT (ares_tac [subsetI,UnionI] 1));
   23.19  qed "Union_upper";
   23.20  
   23.21 -val [prem] = goal Set.thy
   23.22 -    "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
   23.23 +val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
   23.24  by (rtac subsetI 1);
   23.25  by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
   23.26  qed "Union_least";
   23.27  
   23.28  (** General union **)
   23.29  
   23.30 -val prems = goal Set.thy
   23.31 -    "a:A ==> B(a) <= (UN x:A. B(x))";
   23.32 -by (REPEAT (ares_tac (prems@[UN_I RS subsetI]) 1));
   23.33 +Goal "a:A ==> B(a) <= (UN x:A. B(x))";
   23.34 +by (Blast_tac 1);
   23.35  qed "UN_upper";
   23.36  
   23.37 -val [prem] = goal Set.thy
   23.38 -    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
   23.39 +val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
   23.40  by (rtac subsetI 1);
   23.41  by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
   23.42  qed "UN_least";
   23.43 @@ -45,52 +41,49 @@
   23.44  
   23.45  (*** Big Intersection -- greatest lower bound of a set ***)
   23.46  
   23.47 -goal Set.thy "!!B. B:A ==> Inter(A) <= B";
   23.48 +Goal "B:A ==> Inter(A) <= B";
   23.49  by (Blast_tac 1);
   23.50  qed "Inter_lower";
   23.51  
   23.52 -val [prem] = goal Set.thy
   23.53 -    "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
   23.54 +val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
   23.55  by (rtac (InterI RS subsetI) 1);
   23.56  by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
   23.57  qed "Inter_greatest";
   23.58  
   23.59 -val prems = goal Set.thy "a:A ==> (INT x:A. B(x)) <= B(a)";
   23.60 -by (rtac subsetI 1);
   23.61 -by (REPEAT (resolve_tac prems 1 ORELSE etac INT_D 1));
   23.62 +Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
   23.63 +by (Blast_tac 1);
   23.64  qed "INT_lower";
   23.65  
   23.66 -val [prem] = goal Set.thy
   23.67 -    "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
   23.68 +val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
   23.69  by (rtac (INT_I RS subsetI) 1);
   23.70  by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
   23.71  qed "INT_greatest";
   23.72  
   23.73  (*** Finite Union -- the least upper bound of 2 sets ***)
   23.74  
   23.75 -goal Set.thy "A <= A Un B";
   23.76 +Goal "A <= A Un B";
   23.77  by (Blast_tac 1);
   23.78  qed "Un_upper1";
   23.79  
   23.80 -goal Set.thy "B <= A Un B";
   23.81 +Goal "B <= A Un B";
   23.82  by (Blast_tac 1);
   23.83  qed "Un_upper2";
   23.84  
   23.85 -goal Set.thy "!!C. [| A<=C;  B<=C |] ==> A Un B <= C";
   23.86 +Goal "[| A<=C;  B<=C |] ==> A Un B <= C";
   23.87  by (Blast_tac 1);
   23.88  qed "Un_least";
   23.89  
   23.90  (*** Finite Intersection -- the greatest lower bound of 2 sets *)
   23.91  
   23.92 -goal Set.thy "A Int B <= A";
   23.93 +Goal "A Int B <= A";
   23.94  by (Blast_tac 1);
   23.95  qed "Int_lower1";
   23.96  
   23.97 -goal Set.thy "A Int B <= B";
   23.98 +Goal "A Int B <= B";
   23.99  by (Blast_tac 1);
  23.100  qed "Int_lower2";
  23.101  
  23.102 -goal Set.thy "!!C. [| C<=A;  C<=B |] ==> C <= A Int B";
  23.103 +Goal "[| C<=A;  C<=B |] ==> C <= A Int B";
  23.104  by (Blast_tac 1);
  23.105  qed "Int_greatest";
  23.106  
  23.107 @@ -101,14 +94,14 @@
  23.108  
  23.109  (*** Monotonicity ***)
  23.110  
  23.111 -val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
  23.112 +Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
  23.113  by (rtac Un_least 1);
  23.114 -by (rtac (Un_upper1 RS (prem RS monoD)) 1);
  23.115 -by (rtac (Un_upper2 RS (prem RS monoD)) 1);
  23.116 +by (etac (Un_upper1 RSN (2,monoD)) 1);
  23.117 +by (etac (Un_upper2 RSN (2,monoD)) 1);
  23.118  qed "mono_Un";
  23.119  
  23.120 -val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
  23.121 +Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
  23.122  by (rtac Int_greatest 1);
  23.123 -by (rtac (Int_lower1 RS (prem RS monoD)) 1);
  23.124 -by (rtac (Int_lower2 RS (prem RS monoD)) 1);
  23.125 +by (etac (Int_lower1 RSN (2,monoD)) 1);
  23.126 +by (etac (Int_lower2 RSN (2,monoD)) 1);
  23.127  qed "mono_Int";