removal of batch-style proofs
authorpaulson
Fri Jun 30 12:51:30 2000 +0200 (2000-06-30)
changeset 92116236c5285bd8
parent 9210 8a080ade1a8c
child 9212 4afe62073b41
removal of batch-style proofs
src/ZF/Cardinal.ML
src/ZF/Epsilon.ML
src/ZF/Finite.ML
src/ZF/InfDatatype.ML
src/ZF/OrdQuant.ML
src/ZF/Perm.ML
src/ZF/QPair.ML
src/ZF/QUniv.ML
src/ZF/ROOT.ML
src/ZF/Trancl.ML
src/ZF/ZF.ML
src/ZF/domrange.ML
src/ZF/func.ML
src/ZF/pair.ML
src/ZF/subset.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/Cardinal.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/Cardinal.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -219,12 +219,13 @@
     1.4  qed "less_LeastE";
     1.5  
     1.6  (*Easier to apply than LeastI: conclusion has only one occurrence of P*)
     1.7 -qed_goal "LeastI2" Cardinal.thy
     1.8 -    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
     1.9 - (fn prems => [ resolve_tac prems 1, 
    1.10 -                rtac LeastI 1, 
    1.11 -                resolve_tac prems 1, 
    1.12 -                resolve_tac prems 1 ]);
    1.13 +val prems = goal Cardinal.thy
    1.14 +    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))";
    1.15 +by (resolve_tac prems 1);
    1.16 +by (rtac LeastI 1);
    1.17 +by (resolve_tac prems 1);
    1.18 +by (resolve_tac prems 1) ;
    1.19 +qed "LeastI2";
    1.20  
    1.21  (*If there is no such P then LEAST is vacuously 0*)
    1.22  Goalw [Least_def]
     2.1 --- a/src/ZF/Epsilon.ML	Fri Jun 30 12:49:11 2000 +0200
     2.2 +++ b/src/ZF/Epsilon.ML	Fri Jun 30 12:51:30 2000 +0200
     2.3 @@ -42,7 +42,7 @@
     2.4  bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
     2.5  
     2.6  (*Epsilon induction*)
     2.7 -val prems = goal Epsilon.thy
     2.8 +val prems = Goal
     2.9      "[| !!x. ALL y:x. P(y) ==> P(x) |]  ==>  P(a)";
    2.10  by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
    2.11  by (eresolve_tac prems 1);
    2.12 @@ -74,7 +74,7 @@
    2.13  qed "eclose_least";
    2.14  
    2.15  (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    2.16 -val [major,base,step] = goal Epsilon.thy
    2.17 +val [major,base,step] = Goal
    2.18      "[| a: eclose(b);                                           \
    2.19  \       !!y.   [| y: b |] ==> P(y);                             \
    2.20  \       !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)        \
    2.21 @@ -126,10 +126,10 @@
    2.22                                    jmemi RSN (2,mem_eclose_sing_trans)]) 1);
    2.23  qed "wfrec_eclose_eq";
    2.24  
    2.25 -val [prem] = goal Epsilon.thy
    2.26 +Goal
    2.27      "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
    2.28  by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
    2.29 -by (rtac (prem RS arg_into_eclose_sing) 1);
    2.30 +by (etac arg_into_eclose_sing 1);
    2.31  qed "wfrec_eclose_eq2";
    2.32  
    2.33  Goalw [transrec_def]
    2.34 @@ -140,13 +140,13 @@
    2.35  qed "transrec";
    2.36  
    2.37  (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
    2.38 -val rew::prems = goal Epsilon.thy
    2.39 +val rew::prems = Goal
    2.40      "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
    2.41  by (rewtac rew);
    2.42  by (REPEAT (resolve_tac (prems@[transrec]) 1));
    2.43  qed "def_transrec";
    2.44  
    2.45 -val prems = goal Epsilon.thy
    2.46 +val prems = Goal
    2.47      "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
    2.48  \    |]  ==> transrec(a,H) : B(a)";
    2.49  by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
    2.50 @@ -159,7 +159,7 @@
    2.51  by (rtac (succI1 RS singleton_subsetI) 1);
    2.52  qed "eclose_sing_Ord";
    2.53  
    2.54 -val prems = goal Epsilon.thy
    2.55 +val prems = Goal
    2.56      "[| j: i;  Ord(i);  \
    2.57  \       !!x u. [| x: i;  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
    2.58  \    |]  ==> transrec(j,H) : B(j)";
    2.59 @@ -186,8 +186,8 @@
    2.60  qed "Ord_rank";
    2.61  Addsimps [Ord_rank];
    2.62  
    2.63 -val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
    2.64 -by (rtac (major RS trans_induct) 1);
    2.65 +Goal "Ord(i) ==> rank(i) = i";
    2.66 +by (etac trans_induct 1);
    2.67  by (stac rank 1);
    2.68  by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
    2.69  qed "rank_of_Ord";
    2.70 @@ -199,8 +199,8 @@
    2.71  by Auto_tac;
    2.72  qed "rank_lt";
    2.73  
    2.74 -val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
    2.75 -by (rtac (major RS eclose_induct_down) 1);
    2.76 +Goal "a: eclose(b) ==> rank(a) < rank(b)";
    2.77 +by (etac eclose_induct_down 1);
    2.78  by (etac rank_lt 1);
    2.79  by (etac (rank_lt RS lt_trans) 1);
    2.80  by (assume_tac 1);
     3.1 --- a/src/ZF/Finite.ML	Fri Jun 30 12:49:11 2000 +0200
     3.2 +++ b/src/ZF/Finite.ML	Fri Jun 30 12:51:30 2000 +0200
     3.3 @@ -48,8 +48,8 @@
     3.4  
     3.5  
     3.6  (*The union of a set of finite sets is finite.*)
     3.7 -val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
     3.8 -by (rtac (major RS Fin_induct) 1);
     3.9 +Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
    3.10 +by (etac Fin_induct 1);
    3.11  by (ALLGOALS Asm_simp_tac);
    3.12  qed "Fin_UnionI";
    3.13  
     4.1 --- a/src/ZF/InfDatatype.ML	Fri Jun 30 12:49:11 2000 +0200
     4.2 +++ b/src/ZF/InfDatatype.ML	Fri Jun 30 12:51:30 2000 +0200
     4.3 @@ -71,9 +71,9 @@
     4.4  qed "Card_fun_in_Vcsucc";
     4.5  
     4.6  (*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*)
     4.7 -qed_goal "Limit_csucc" InfDatatype.thy
     4.8 -    "!!K. InfCard(K) ==> Limit(csucc(K))"
     4.9 -  (fn _ => [etac (InfCard_csucc RS InfCard_is_Limit) 1]);
    4.10 +Goal "InfCard(K) ==> Limit(csucc(K))";
    4.11 +by (etac (InfCard_csucc RS InfCard_is_Limit) 1);
    4.12 +qed "Limit_csucc";
    4.13  
    4.14  bind_thm ("Pair_in_Vcsucc",  Limit_csucc RSN (3, Pair_in_VLimit));
    4.15  bind_thm ("Inl_in_Vcsucc",   Limit_csucc RSN (2, Inl_in_VLimit));
     5.1 --- a/src/ZF/OrdQuant.ML	Fri Jun 30 12:49:11 2000 +0200
     5.2 +++ b/src/ZF/OrdQuant.ML	Fri Jun 30 12:51:30 2000 +0200
     5.3 @@ -7,23 +7,23 @@
     5.4  
     5.5  (*** universal quantifier for ordinals ***)
     5.6  
     5.7 -qed_goalw "oallI" thy [oall_def]
     5.8 -    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
     5.9 - (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
    5.10 +val prems = Goalw [oall_def] 
    5.11 +    "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)";
    5.12 +by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
    5.13 +qed "oallI";
    5.14  
    5.15 -qed_goalw "ospec" thy [oall_def]
    5.16 -    "[| ALL x<A. P(x);  x<A |] ==> P(x)"
    5.17 - (fn major::prems=>
    5.18 -  [ (rtac (major RS spec RS mp) 1),
    5.19 -    (resolve_tac prems 1) ]);
    5.20 +Goalw [oall_def] "[| ALL x<A. P(x);  x<A |] ==> P(x)";
    5.21 +by (etac (spec RS mp) 1);
    5.22 +by (assume_tac 1) ;
    5.23 +qed "ospec";
    5.24  
    5.25 -qed_goalw "oallE" thy [oall_def]
    5.26 -    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q"
    5.27 - (fn major::prems=>
    5.28 -  [ (rtac (major RS allE) 1),
    5.29 -    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
    5.30 +val major::prems = Goalw [oall_def] 
    5.31 +    "[| ALL x<A. P(x);  P(x) ==> Q;  ~x<A ==> Q |] ==> Q";
    5.32 +by (rtac (major RS allE) 1);
    5.33 +by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
    5.34 +qed "oallE";
    5.35  
    5.36 -val major::prems= goal thy
    5.37 +val major::prems = Goal
    5.38      "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q";
    5.39  by (rtac (major RS oallE) 1);
    5.40  by (REPEAT (eresolve_tac prems 1)) ;
    5.41 @@ -35,16 +35,18 @@
    5.42  qed "oall_simp";
    5.43  
    5.44  (*Congruence rule for rewriting*)
    5.45 -qed_goalw "oall_cong" thy [oall_def]
    5.46 -    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
    5.47 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
    5.48 +val prems = Goalw [oall_def] 
    5.49 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')";
    5.50 +by (simp_tac (simpset() addsimps prems) 1) ;
    5.51 +qed "oall_cong";
    5.52  
    5.53  
    5.54  (*** existential quantifier for ordinals ***)
    5.55  
    5.56 -qed_goalw "oexI" thy [oex_def]
    5.57 -    "[| P(x);  x<A |] ==> EX x<A. P(x)"
    5.58 - (fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
    5.59 +val prems = Goalw [oex_def] 
    5.60 +    "[| P(x);  x<A |] ==> EX x<A. P(x)";
    5.61 +by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ;
    5.62 +qed "oexI";
    5.63  
    5.64  (*Not of the general form for such rules; ~EX has become ALL~ *)
    5.65  val prems = Goal
    5.66 @@ -53,35 +55,36 @@
    5.67  by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
    5.68  qed "oexCI";
    5.69  
    5.70 -qed_goalw "oexE" thy [oex_def]
    5.71 +val major::prems = Goalw [oex_def] 
    5.72      "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q \
    5.73 -\    |] ==> Q"
    5.74 - (fn major::prems=>
    5.75 -  [ (rtac (major RS exE) 1),
    5.76 -    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
    5.77 +\    |] ==> Q";
    5.78 +by (rtac (major RS exE) 1);
    5.79 +by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
    5.80 +qed "oexE";
    5.81  
    5.82 -qed_goalw "oex_cong" thy [oex_def]
    5.83 +val prems = Goalw [oex_def] 
    5.84      "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) \
    5.85 -\    |] ==> oex(a,P) <-> oex(a',P')"
    5.86 - (fn prems=> [ (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ]);
    5.87 +\    |] ==> oex(a,P) <-> oex(a',P')";
    5.88 +by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ;
    5.89 +qed "oex_cong";
    5.90  
    5.91  
    5.92  (*** Rules for Ordinal-Indexed Unions ***)
    5.93  
    5.94 -qed_goalw "OUN_I" thy [OUnion_def]
    5.95 -        "!!i. [| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
    5.96 - (fn _=> [ fast_tac (claset() addSEs [ltE]) 1 ]);
    5.97 +Goalw [OUnion_def] "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))";
    5.98 +by (blast_tac (claset() addSEs [ltE]) 1);
    5.99 +qed "OUN_I";
   5.100  
   5.101 -qed_goalw "OUN_E" thy [OUnion_def]
   5.102 -    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
   5.103 - (fn major::prems=>
   5.104 -  [ (rtac (major RS CollectE) 1),
   5.105 -    (rtac UN_E 1),
   5.106 -    (REPEAT (ares_tac (ltI::prems) 1)) ]);
   5.107 +val major::prems = Goalw [OUnion_def] 
   5.108 +    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R";
   5.109 +by (rtac (major RS CollectE) 1);
   5.110 +by (rtac UN_E 1);
   5.111 +by (REPEAT (ares_tac (ltI::prems) 1)) ;
   5.112 +qed "OUN_E";
   5.113  
   5.114 -qed_goalw "OUN_iff" thy [oex_def]
   5.115 -    "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
   5.116 - (fn _=> [ (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ]);
   5.117 +Goalw [oex_def] "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))";
   5.118 +by (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ;
   5.119 +qed "OUN_iff";
   5.120  
   5.121  val prems = Goal
   5.122      "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";
     6.1 --- a/src/ZF/Perm.ML	Fri Jun 30 12:49:11 2000 +0200
     6.2 +++ b/src/ZF/Perm.ML	Fri Jun 30 12:51:30 2000 +0200
     6.3 @@ -25,7 +25,7 @@
     6.4  
     6.5  (** A function with a right inverse is a surjection **)
     6.6  
     6.7 -val prems = goalw Perm.thy [surj_def]
     6.8 +val prems = Goalw [surj_def]
     6.9      "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y \
    6.10  \    |] ==> f: surj(A,B)";
    6.11  by (blast_tac (claset() addIs prems) 1);
    6.12 @@ -92,7 +92,7 @@
    6.13  (* f: bij(A,B) ==> f: A->B *)
    6.14  bind_thm ("bij_is_fun", bij_is_inj RS inj_is_fun);
    6.15  
    6.16 -val prems = goalw Perm.thy [bij_def]
    6.17 +val prems = Goalw [bij_def]
    6.18      "[| !!x. x:A ==> c(x): B;           \
    6.19  \       !!y. y:B ==> d(y): A;           \
    6.20  \       !!x. x:A ==> d(c(x)) = x;       \
    6.21 @@ -111,11 +111,11 @@
    6.22  
    6.23  (** Identity function **)
    6.24  
    6.25 -val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";  
    6.26 -by (rtac (prem RS lamI) 1);
    6.27 +Goalw [id_def] "a:A ==> <a,a> : id(A)";  
    6.28 +by (etac lamI 1);
    6.29  qed "idI";
    6.30  
    6.31 -val major::prems = goalw Perm.thy [id_def]
    6.32 +val major::prems = Goalw [id_def]
    6.33      "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P  \
    6.34  \    |] ==>  P";  
    6.35  by (rtac (major RS lamE) 1);
    6.36 @@ -133,8 +133,8 @@
    6.37  
    6.38  Addsimps [id_conv];
    6.39  
    6.40 -val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
    6.41 -by (rtac (prem RS lam_mono) 1);
    6.42 +Goalw [id_def] "A<=B ==> id(A) <= id(B)";
    6.43 +by (etac lam_mono 1);
    6.44  qed "id_mono";
    6.45  
    6.46  Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
    6.47 @@ -233,7 +233,7 @@
    6.48  by (Blast_tac 1);
    6.49  qed "compI";
    6.50  
    6.51 -val prems = goalw Perm.thy [comp_def]
    6.52 +val prems = Goalw [comp_def]
    6.53      "[| xz : r O s;  \
    6.54  \       !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P \
    6.55  \    |] ==> P";
     7.1 --- a/src/ZF/QPair.ML	Fri Jun 30 12:49:11 2000 +0200
     7.2 +++ b/src/ZF/QPair.ML	Fri Jun 30 12:51:30 2000 +0200
     7.3 @@ -16,53 +16,49 @@
     7.4      is not a limit ordinal? 
     7.5  *)
     7.6  
     7.7 -open QPair;
     7.8 -
     7.9  (**** Quine ordered pairing ****)
    7.10  
    7.11  (** Lemmas for showing that <a;b> uniquely determines a and b **)
    7.12  
    7.13 -qed_goalw "QPair_empty" thy [QPair_def]
    7.14 -    "<0;0> = 0"
    7.15 - (fn _=> [Simp_tac 1]);
    7.16 +Goalw [QPair_def] "<0;0> = 0";
    7.17 +by (Simp_tac 1);
    7.18 +qed "QPair_empty";
    7.19  
    7.20 -qed_goalw "QPair_iff" thy [QPair_def]
    7.21 -    "<a;b> = <c;d> <-> a=c & b=d"
    7.22 - (fn _=> [rtac sum_equal_iff 1]);
    7.23 +Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d";
    7.24 +by (rtac sum_equal_iff 1);
    7.25 +qed "QPair_iff";
    7.26  
    7.27 -bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE));
    7.28 +bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE);
    7.29  
    7.30  Addsimps [QPair_empty, QPair_iff];
    7.31  AddSEs   [QPair_inject];
    7.32  
    7.33 -val [major]= goal thy "<a;b> = <c;d> ==> a=c";
    7.34 -by (rtac (major RS QPair_inject) 1);
    7.35 -by (assume_tac 1) ;
    7.36 +Goal "<a;b> = <c;d> ==> a=c";
    7.37 +by (Blast_tac 1) ;
    7.38  qed "QPair_inject1";
    7.39  
    7.40 -val [major]= goal thy "<a;b> = <c;d> ==> b=d";
    7.41 -by (rtac (major RS QPair_inject) 1);
    7.42 -by (assume_tac 1) ;
    7.43 +Goal "<a;b> = <c;d> ==> b=d";
    7.44 +by (Blast_tac 1) ;
    7.45  qed "QPair_inject2";
    7.46  
    7.47  
    7.48  (*** QSigma: Disjoint union of a family of sets
    7.49       Generalizes Cartesian product ***)
    7.50  
    7.51 -qed_goalw "QSigmaI" thy [QSigma_def]
    7.52 -    "!!A B. [| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
    7.53 - (fn _ => [ Blast_tac 1 ]);
    7.54 +Goalw [QSigma_def] "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)";
    7.55 +by (Blast_tac 1) ;
    7.56 +qed "QSigmaI";
    7.57  
    7.58  AddSIs [QSigmaI];
    7.59  
    7.60  (*The general elimination rule*)
    7.61 -qed_goalw "QSigmaE" thy [QSigma_def]
    7.62 +val major::prems= Goalw [QSigma_def] 
    7.63      "[| c: QSigma(A,B);  \
    7.64  \       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
    7.65 -\    |] ==> P"
    7.66 - (fn major::prems=>
    7.67 -  [ (cut_facts_tac [major] 1),
    7.68 -    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
    7.69 +\    |] ==> P";
    7.70 +by (cut_facts_tac [major] 1);
    7.71 +by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
    7.72 +qed "QSigmaE";
    7.73  
    7.74  (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
    7.75  
    7.76 @@ -71,23 +67,22 @@
    7.77                    THEN prune_params_tac)
    7.78        (inst "c" "<a;b>" QSigmaE);  
    7.79  
    7.80 -val [major]= goal thy "<a;b> : QSigma(A,B) ==> a : A";
    7.81 -by (rtac (major RS QSigmaE2) 1);
    7.82 -by (assume_tac 1) ;
    7.83 +AddSEs [QSigmaE2, QSigmaE];
    7.84 +
    7.85 +Goal "<a;b> : QSigma(A,B) ==> a : A";
    7.86 +by (Blast_tac 1) ;
    7.87  qed "QSigmaD1";
    7.88  
    7.89 -val [major]= goal thy "<a;b> : QSigma(A,B) ==> b : B(a)";
    7.90 -by (rtac (major RS QSigmaE2) 1);
    7.91 -by (assume_tac 1) ;
    7.92 +Goal "<a;b> : QSigma(A,B) ==> b : B(a)";
    7.93 +by (Blast_tac 1) ;
    7.94  qed "QSigmaD2";
    7.95  
    7.96 -AddSEs [QSigmaE2, QSigmaE];
    7.97  
    7.98 -
    7.99 -qed_goalw "QSigma_cong" thy [QSigma_def]
   7.100 +val prems= Goalw [QSigma_def] 
   7.101      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
   7.102 -\    QSigma(A,B) = QSigma(A',B')"
   7.103 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
   7.104 +\    QSigma(A,B) = QSigma(A',B')";
   7.105 +by (simp_tac (simpset() addsimps prems) 1) ;
   7.106 +qed "QSigma_cong";
   7.107  
   7.108  Goal "QSigma(0,B) = 0";
   7.109  by (Blast_tac 1) ;
   7.110 @@ -102,13 +97,13 @@
   7.111  
   7.112  (*** Projections: qfst, qsnd ***)
   7.113  
   7.114 -qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
   7.115 - (fn _=> 
   7.116 -  [ (Blast_tac 1) ]);
   7.117 +Goalw [qfst_def]  "qfst(<a;b>) = a";
   7.118 +by (Blast_tac 1) ;
   7.119 +qed "qfst_conv";
   7.120  
   7.121 -qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
   7.122 - (fn _=> 
   7.123 -  [ (Blast_tac 1) ]);
   7.124 +Goalw [qsnd_def]  "qsnd(<a;b>) = b";
   7.125 +by (Blast_tac 1) ;
   7.126 +qed "qsnd_conv";
   7.127  
   7.128  Addsimps [qfst_conv, qsnd_conv];
   7.129  
   7.130 @@ -133,7 +128,7 @@
   7.131  qed "qsplit";
   7.132  Addsimps [qsplit];
   7.133  
   7.134 -val major::prems= goal thy
   7.135 +val major::prems= Goal
   7.136      "[|  p:QSigma(A,B);   \
   7.137  \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
   7.138  \    |] ==> qsplit(%x y. c(x,y), p) : C(p)";
   7.139 @@ -153,7 +148,7 @@
   7.140  by (Asm_simp_tac 1);
   7.141  qed "qsplitI";
   7.142  
   7.143 -val major::sigma::prems = goalw thy [qsplit_def]
   7.144 +val major::sigma::prems = Goalw [qsplit_def]
   7.145      "[| qsplit(R,z);  z:QSigma(A,B);                    \
   7.146  \       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
   7.147  \   |] ==> P";
   7.148 @@ -170,23 +165,23 @@
   7.149  
   7.150  (*** qconverse ***)
   7.151  
   7.152 -qed_goalw "qconverseI" thy [qconverse_def]
   7.153 -    "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
   7.154 - (fn _ => [ (Blast_tac 1) ]);
   7.155 +Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)";
   7.156 +by (Blast_tac 1) ;
   7.157 +qed "qconverseI";
   7.158  
   7.159 -qed_goalw "qconverseD" thy [qconverse_def]
   7.160 -    "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
   7.161 - (fn _ => [ (Blast_tac 1) ]);
   7.162 +Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r";
   7.163 +by (Blast_tac 1) ;
   7.164 +qed "qconverseD";
   7.165  
   7.166 -qed_goalw "qconverseE" thy [qconverse_def]
   7.167 +val [major,minor]= Goalw [qconverse_def] 
   7.168      "[| yx : qconverse(r);  \
   7.169  \       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
   7.170 -\    |] ==> P"
   7.171 - (fn [major,minor]=>
   7.172 -  [ (rtac (major RS ReplaceE) 1),
   7.173 -    (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   7.174 -    (hyp_subst_tac 1),
   7.175 -    (assume_tac 1) ]);
   7.176 +\    |] ==> P";
   7.177 +by (rtac (major RS ReplaceE) 1);
   7.178 +by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
   7.179 +by (hyp_subst_tac 1);
   7.180 +by (assume_tac 1) ;
   7.181 +qed "qconverseE";
   7.182  
   7.183  AddSIs [qconverseI];
   7.184  AddSEs [qconverseD, qconverseE];
   7.185 @@ -224,7 +219,7 @@
   7.186  
   7.187  (** Elimination rules **)
   7.188  
   7.189 -val major::prems = goalw thy qsum_defs
   7.190 +val major::prems = Goalw qsum_defs
   7.191      "[| u: A <+> B;  \
   7.192  \       !!x. [| x:A;  u=QInl(x) |] ==> P; \
   7.193  \       !!y. [| y:B;  u=QInr(y) |] ==> P \
   7.194 @@ -304,7 +299,7 @@
   7.195  
   7.196  Addsimps [qcase_QInl, qcase_QInr];
   7.197  
   7.198 -val major::prems = goal thy
   7.199 +val major::prems = Goal
   7.200      "[| u: A <+> B; \
   7.201  \       !!x. x: A ==> c(x): C(QInl(x));   \
   7.202  \       !!y. y: B ==> d(y): C(QInr(y)) \
     8.1 --- a/src/ZF/QUniv.ML	Fri Jun 30 12:49:11 2000 +0200
     8.2 +++ b/src/ZF/QUniv.ML	Fri Jun 30 12:51:30 2000 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      ZF/quniv
     8.5 +(*  Title:      ZF/QUniv
     8.6      ID:         $Id$
     8.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.8      Copyright   1993  University of Cambridge
     8.9 @@ -8,17 +8,14 @@
    8.10  
    8.11  (** Properties involving Transset and Sum **)
    8.12  
    8.13 -val [prem1,prem2] = goalw QUniv.thy [sum_def]
    8.14 -    "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    8.15 -by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1);
    8.16 -by (REPEAT (etac (prem1 RS Transset_includes_range) 1
    8.17 -     ORELSE resolve_tac [conjI, singletonI] 1));
    8.18 +Goalw [sum_def] "[| Transset(C); A+B <= C |] ==> A <= C & B <= C";
    8.19 +by (dtac (Un_subset_iff RS iffD1) 1);
    8.20 +by (blast_tac (claset() addDs [Transset_includes_range]) 1);
    8.21  qed "Transset_includes_summands";
    8.22  
    8.23 -val [prem] = goalw QUniv.thy [sum_def]
    8.24 -    "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    8.25 +Goalw [sum_def] "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    8.26  by (stac Int_Un_distrib 1);
    8.27 -by (blast_tac (claset() addSDs [prem RS Transset_Pair_D]) 1);
    8.28 +by (blast_tac (claset() addDs [Transset_Pair_D]) 1);
    8.29  qed "Transset_sum_Int_subset";
    8.30  
    8.31  (** Introduction and elimination rules avoid tiresome folding/unfolding **)
     9.1 --- a/src/ZF/ROOT.ML	Fri Jun 30 12:49:11 2000 +0200
     9.2 +++ b/src/ZF/ROOT.ML	Fri Jun 30 12:51:30 2000 +0200
     9.3 @@ -18,7 +18,6 @@
     9.4  (*Add user sections for inductive/datatype definitions*)
     9.5  use     "thy_syntax";
     9.6  
     9.7 -use_thy "Let";
     9.8  use_thy "ZF";
     9.9  use     "Tools/typechk";
    9.10  use_thy "mono";
    9.11 @@ -28,7 +27,6 @@
    9.12  use     "Tools/inductive_package";
    9.13  use     "Tools/induct_tacs";
    9.14  use     "Tools/primrec_package";
    9.15 -use_thy "Inductive";
    9.16  use_thy "QUniv";
    9.17  use     "Tools/datatype_package";
    9.18  
    10.1 --- a/src/ZF/Trancl.ML	Fri Jun 30 12:49:11 2000 +0200
    10.2 +++ b/src/ZF/Trancl.ML	Fri Jun 30 12:51:30 2000 +0200
    10.3 @@ -133,8 +133,7 @@
    10.4  qed "r_subset_trancl";
    10.5  
    10.6  (*intro rule by definition: from r^* and r  *)
    10.7 -Goalw [trancl_def]
    10.8 -    "!!r. [| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
    10.9 +Goalw [trancl_def] "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
   10.10  by (Blast_tac 1);
   10.11  qed "rtrancl_into_trancl1";
   10.12  
    11.1 --- a/src/ZF/ZF.ML	Fri Jun 30 12:49:11 2000 +0200
    11.2 +++ b/src/ZF/ZF.ML	Fri Jun 30 12:51:30 2000 +0200
    11.3 @@ -15,21 +15,21 @@
    11.4  
    11.5  (*** Bounded universal quantifier ***)
    11.6  
    11.7 -qed_goalw "ballI" ZF.thy [Ball_def]
    11.8 -    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
    11.9 - (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
   11.10 +val prems= Goalw [Ball_def] 
   11.11 +    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
   11.12 +by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
   11.13 +qed "ballI";
   11.14  
   11.15 -qed_goalw "bspec" ZF.thy [Ball_def]
   11.16 -    "[| ALL x:A. P(x);  x: A |] ==> P(x)"
   11.17 - (fn major::prems=>
   11.18 -  [ (rtac (major RS spec RS mp) 1),
   11.19 -    (resolve_tac prems 1) ]);
   11.20 +Goalw [Ball_def] "[| ALL x:A. P(x);  x: A |] ==> P(x)";
   11.21 +by (etac (spec RS mp) 1);
   11.22 +by (assume_tac 1) ;
   11.23 +qed "bspec";
   11.24  
   11.25 -qed_goalw "ballE" ZF.thy [Ball_def]
   11.26 -    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q"
   11.27 - (fn major::prems=>
   11.28 -  [ (rtac (major RS allE) 1),
   11.29 -    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
   11.30 +val major::prems= Goalw [Ball_def] 
   11.31 +    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
   11.32 +by (rtac (major RS allE) 1);
   11.33 +by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
   11.34 +qed "ballE";
   11.35  
   11.36  (*Used in the datatype package*)
   11.37  Goal "[| x: A;  ALL x:A. P(x) |] ==> P(x)";
   11.38 @@ -57,9 +57,10 @@
   11.39  Addsimps [ball_triv];
   11.40  
   11.41  (*Congruence rule for rewriting*)
   11.42 -qed_goalw "ball_cong" ZF.thy [Ball_def]
   11.43 -    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
   11.44 - (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
   11.45 +val prems= Goalw [Ball_def] 
   11.46 +    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')";
   11.47 +by (simp_tac (FOL_ss addsimps prems) 1) ;
   11.48 +qed "ball_cong";
   11.49  
   11.50  (*** Bounded existential quantifier ***)
   11.51  
   11.52 @@ -78,12 +79,12 @@
   11.53  by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
   11.54  qed "bexCI";
   11.55  
   11.56 -qed_goalw "bexE" ZF.thy [Bex_def]
   11.57 +val major::prems= Goalw [Bex_def] 
   11.58      "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q \
   11.59 -\    |] ==> Q"
   11.60 - (fn major::prems=>
   11.61 -  [ (rtac (major RS exE) 1),
   11.62 -    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
   11.63 +\    |] ==> Q";
   11.64 +by (rtac (major RS exE) 1);
   11.65 +by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
   11.66 +qed "bexE";
   11.67  
   11.68  AddIs  [bexI];  
   11.69  AddSEs [bexE];
   11.70 @@ -94,32 +95,34 @@
   11.71  qed "bex_triv";
   11.72  Addsimps [bex_triv];
   11.73  
   11.74 -qed_goalw "bex_cong" ZF.thy [Bex_def]
   11.75 +val prems= Goalw [Bex_def] 
   11.76      "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
   11.77 -\    |] ==> Bex(A,P) <-> Bex(A',P')"
   11.78 - (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
   11.79 +\    |] ==> Bex(A,P) <-> Bex(A',P')";
   11.80 +by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ;
   11.81 +qed "bex_cong";
   11.82  
   11.83  Addcongs [ball_cong, bex_cong];
   11.84  
   11.85  
   11.86  (*** Rules for subsets ***)
   11.87  
   11.88 -qed_goalw "subsetI" ZF.thy [subset_def]
   11.89 -    "(!!x. x:A ==> x:B) ==> A <= B"
   11.90 - (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
   11.91 +val prems= Goalw [subset_def] 
   11.92 +    "(!!x. x:A ==> x:B) ==> A <= B";
   11.93 +by (REPEAT (ares_tac (prems @ [ballI]) 1)) ;
   11.94 +qed "subsetI";
   11.95  
   11.96  (*Rule in Modus Ponens style [was called subsetE] *)
   11.97 -qed_goalw "subsetD" ZF.thy [subset_def] "[| A <= B;  c:A |] ==> c:B"
   11.98 - (fn major::prems=>
   11.99 -  [ (rtac (major RS bspec) 1),
  11.100 -    (resolve_tac prems 1) ]);
  11.101 +Goalw [subset_def]  "[| A <= B;  c:A |] ==> c:B";
  11.102 +by (etac bspec 1);
  11.103 +by (assume_tac 1) ;
  11.104 +qed "subsetD";
  11.105  
  11.106  (*Classical elimination rule*)
  11.107 -qed_goalw "subsetCE" ZF.thy [subset_def]
  11.108 -    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P"
  11.109 - (fn major::prems=>
  11.110 -  [ (rtac (major RS ballE) 1),
  11.111 -    (REPEAT (eresolve_tac prems 1)) ]);
  11.112 +val major::prems= Goalw [subset_def] 
  11.113 +    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
  11.114 +by (rtac (major RS ballE) 1);
  11.115 +by (REPEAT (eresolve_tac prems 1)) ;
  11.116 +qed "subsetCE";
  11.117  
  11.118  AddSIs [subsetI];
  11.119  AddEs  [subsetCE, subsetD];
  11.120 @@ -155,9 +158,10 @@
  11.121  qed "subset_trans";
  11.122  
  11.123  (*Useful for proving A<=B by rewriting in some cases*)
  11.124 -qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def]
  11.125 -     "A<=B <-> (ALL x. x:A --> x:B)"
  11.126 - (fn _=> [ (rtac iff_refl 1) ]);
  11.127 +Goalw [subset_def,Ball_def] 
  11.128 +     "A<=B <-> (ALL x. x:A --> x:B)";
  11.129 +by (rtac iff_refl 1) ;
  11.130 +qed "subset_iff";
  11.131  
  11.132  
  11.133  (*** Rules for equality ***)
  11.134 @@ -199,12 +203,12 @@
  11.135  
  11.136  (*** Rules for Replace -- the derived form of replacement ***)
  11.137  
  11.138 -qed_goalw "Replace_iff" ZF.thy [Replace_def]
  11.139 -    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
  11.140 - (fn _=>
  11.141 -  [ (rtac (replacement RS iff_trans) 1),
  11.142 -    (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
  11.143 -        ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
  11.144 +Goalw [Replace_def] 
  11.145 +    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))";
  11.146 +by (rtac (replacement RS iff_trans) 1);
  11.147 +by (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1 
  11.148 +     ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ;
  11.149 +qed "Replace_iff";
  11.150  
  11.151  (*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
  11.152  val prems = Goal
  11.153 @@ -249,9 +253,9 @@
  11.154  
  11.155  (*** Rules for RepFun ***)
  11.156  
  11.157 -qed_goalw "RepFunI" ZF.thy [RepFun_def]
  11.158 -    "!!a A. a : A ==> f(a) : {f(x). x:A}"
  11.159 - (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
  11.160 +Goalw [RepFun_def] "a : A ==> f(a) : {f(x). x:A}";
  11.161 +by (REPEAT (ares_tac [ReplaceI,refl] 1)) ;
  11.162 +qed "RepFunI";
  11.163  
  11.164  (*Useful for coinduction proofs*)
  11.165  Goal "[| b=f(a);  a : A |] ==> b : {f(x). x:A}";
  11.166 @@ -259,26 +263,27 @@
  11.167  by (etac RepFunI 1) ;
  11.168  qed "RepFun_eqI";
  11.169  
  11.170 -qed_goalw "RepFunE" ZF.thy [RepFun_def]
  11.171 +val major::prems= Goalw [RepFun_def] 
  11.172      "[| b : {f(x). x:A};  \
  11.173  \       !!x.[| x:A;  b=f(x) |] ==> P |] ==> \
  11.174 -\    P"
  11.175 - (fn major::prems=>
  11.176 -  [ (rtac (major RS ReplaceE) 1),
  11.177 -    (REPEAT (ares_tac prems 1)) ]);
  11.178 +\    P";
  11.179 +by (rtac (major RS ReplaceE) 1);
  11.180 +by (REPEAT (ares_tac prems 1)) ;
  11.181 +qed "RepFunE";
  11.182  
  11.183  AddIs  [RepFun_eqI];  
  11.184  AddSEs [RepFunE];
  11.185  
  11.186 -qed_goalw "RepFun_cong" ZF.thy [RepFun_def]
  11.187 -    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
  11.188 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
  11.189 +val prems= Goalw [RepFun_def] 
  11.190 +    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)";
  11.191 +by (simp_tac (simpset() addsimps prems) 1) ;
  11.192 +qed "RepFun_cong";
  11.193  
  11.194  Addcongs [RepFun_cong];
  11.195  
  11.196 -qed_goalw "RepFun_iff" ZF.thy [Bex_def]
  11.197 -    "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
  11.198 - (fn _ => [(Blast_tac 1)]);
  11.199 +Goalw [Bex_def] "b : {f(x). x:A} <-> (EX x:A. b=f(x))";
  11.200 +by (Blast_tac 1);
  11.201 +qed "RepFun_iff";
  11.202  
  11.203  Goal "{x. x:A} = A";
  11.204  by (Blast_tac 1);
  11.205 @@ -289,9 +294,9 @@
  11.206  (*** Rules for Collect -- forming a subset by separation ***)
  11.207  
  11.208  (*Separation is derivable from Replacement*)
  11.209 -qed_goalw "separation" ZF.thy [Collect_def]
  11.210 -    "a : {x:A. P(x)} <-> a:A & P(a)"
  11.211 - (fn _=> [(Blast_tac 1)]);
  11.212 +Goalw [Collect_def] "a : {x:A. P(x)} <-> a:A & P(a)";
  11.213 +by (Blast_tac 1);
  11.214 +qed "separation";
  11.215  
  11.216  Addsimps [separation];
  11.217  
  11.218 @@ -315,9 +320,10 @@
  11.219  by (assume_tac 1) ;
  11.220  qed "CollectD2";
  11.221  
  11.222 -qed_goalw "Collect_cong" ZF.thy [Collect_def] 
  11.223 -    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
  11.224 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
  11.225 +val prems= Goalw [Collect_def]  
  11.226 +    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)";
  11.227 +by (simp_tac (simpset() addsimps prems) 1) ;
  11.228 +qed "Collect_cong";
  11.229  
  11.230  AddSIs [CollectI];
  11.231  AddSEs [CollectE];
  11.232 @@ -341,9 +347,10 @@
  11.233  (*** Rules for Unions of families ***)
  11.234  (* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
  11.235  
  11.236 -qed_goalw "UN_iff" ZF.thy [Bex_def]
  11.237 -    "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
  11.238 - (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
  11.239 +Goalw [Bex_def] "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))";
  11.240 +by (Simp_tac 1);
  11.241 +by (Blast_tac 1) ;
  11.242 +qed "UN_iff";
  11.243  
  11.244  Addsimps [UN_iff];
  11.245  
  11.246 @@ -377,9 +384,11 @@
  11.247  (*** Rules for Inter ***)
  11.248  
  11.249  (*Not obviously useful towards proving InterI, InterD, InterE*)
  11.250 -qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def]
  11.251 -    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
  11.252 - (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
  11.253 +Goalw [Inter_def,Ball_def] 
  11.254 +    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)";
  11.255 +by (Simp_tac 1);
  11.256 +by (Blast_tac 1) ;
  11.257 +qed "Inter_iff";
  11.258  
  11.259  (* Intersection is well-behaved only if the family is non-empty! *)
  11.260  val prems = Goal
  11.261 @@ -390,16 +399,16 @@
  11.262  
  11.263  (*A "destruct" rule -- every B in C contains A as an element, but
  11.264    A:B can hold when B:C does not!  This rule is analogous to "spec". *)
  11.265 -qed_goalw "InterD" ZF.thy [Inter_def]
  11.266 -    "!!C. [| A : Inter(C);  B : C |] ==> A : B"
  11.267 - (fn _=> [(Blast_tac 1)]);
  11.268 +Goalw [Inter_def] "[| A : Inter(C);  B : C |] ==> A : B";
  11.269 +by (Blast_tac 1);
  11.270 +qed "InterD";
  11.271  
  11.272  (*"Classical" elimination rule -- does not require exhibiting B:C *)
  11.273 -qed_goalw "InterE" ZF.thy [Inter_def]
  11.274 -    "[| A : Inter(C);  B~:C ==> R;  A:B ==> R |] ==> R"
  11.275 - (fn major::prems=>
  11.276 -  [ (rtac (major RS CollectD2 RS ballE) 1),
  11.277 -    (REPEAT (eresolve_tac prems 1)) ]);
  11.278 +val major::prems= Goalw [Inter_def] 
  11.279 +    "[| A : Inter(C);  B~:C ==> R;  A:B ==> R |] ==> R";
  11.280 +by (rtac (major RS CollectD2 RS ballE) 1);
  11.281 +by (REPEAT (eresolve_tac prems 1)) ;
  11.282 +qed "InterE";
  11.283  
  11.284  AddSIs [InterI];
  11.285  AddEs  [InterD, InterE];
  11.286 @@ -407,9 +416,10 @@
  11.287  (*** Rules for Intersections of families ***)
  11.288  (* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
  11.289  
  11.290 -qed_goalw "INT_iff" ZF.thy [Inter_def]
  11.291 -    "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
  11.292 - (fn _=> [ Simp_tac 1, Best_tac 1 ]);
  11.293 +Goalw [Inter_def] "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)";
  11.294 +by (Simp_tac 1);
  11.295 +by (Best_tac 1) ;
  11.296 +qed "INT_iff";
  11.297  
  11.298  val prems = Goal
  11.299      "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))";
    12.1 --- a/src/ZF/domrange.ML	Fri Jun 30 12:49:11 2000 +0200
    12.2 +++ b/src/ZF/domrange.ML	Fri Jun 30 12:51:30 2000 +0200
    12.3 @@ -8,27 +8,27 @@
    12.4  
    12.5  (*** converse ***)
    12.6  
    12.7 -qed_goalw "converse_iff" thy [converse_def]
    12.8 -    "<a,b>: converse(r) <-> <b,a>:r"
    12.9 - (fn _ => [ (Blast_tac 1) ]);
   12.10 +Goalw [converse_def] "<a,b>: converse(r) <-> <b,a>:r";
   12.11 +by (Blast_tac 1) ;
   12.12 +qed "converse_iff";
   12.13  
   12.14 -qed_goalw "converseI" thy [converse_def]
   12.15 -    "!!a b r. <a,b>:r ==> <b,a>:converse(r)"
   12.16 - (fn _ => [ (Blast_tac 1) ]);
   12.17 +Goalw [converse_def] "<a,b>:r ==> <b,a>:converse(r)";
   12.18 +by (Blast_tac 1) ;
   12.19 +qed "converseI";
   12.20  
   12.21 -qed_goalw "converseD" thy [converse_def]
   12.22 -    "!!a b r. <a,b> : converse(r) ==> <b,a> : r"
   12.23 - (fn _ => [ (Blast_tac 1) ]);
   12.24 +Goalw [converse_def] "<a,b> : converse(r) ==> <b,a> : r";
   12.25 +by (Blast_tac 1) ;
   12.26 +qed "converseD";
   12.27  
   12.28 -qed_goalw "converseE" thy [converse_def]
   12.29 +val [major,minor]= Goalw [converse_def] 
   12.30      "[| yx : converse(r);  \
   12.31  \       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
   12.32 -\    |] ==> P"
   12.33 - (fn [major,minor]=>
   12.34 -  [ (rtac (major RS ReplaceE) 1),
   12.35 -    (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   12.36 -    (hyp_subst_tac 1),
   12.37 -    (assume_tac 1) ]);
   12.38 +\    |] ==> P";
   12.39 +by (rtac (major RS ReplaceE) 1);
   12.40 +by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
   12.41 +by (hyp_subst_tac 1);
   12.42 +by (assume_tac 1) ;
   12.43 +qed "converseE";
   12.44  
   12.45  Addsimps [converse_iff];
   12.46  AddSIs [converseI];
   12.47 @@ -52,16 +52,16 @@
   12.48  
   12.49  Addsimps [converse_prod, converse_empty];
   12.50  
   12.51 -val converse_subset_iff = prove_goal thy
   12.52 -  "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
   12.53 - (fn _=> [ (Blast_tac 1) ]);
   12.54 +Goal "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B";
   12.55 +by (Blast_tac 1) ;
   12.56 +qed "converse_subset_iff";
   12.57  
   12.58  
   12.59  (*** domain ***)
   12.60  
   12.61 -qed_goalw "domain_iff" thy [domain_def]
   12.62 -    "a: domain(r) <-> (EX y. <a,y>: r)"
   12.63 - (fn _=> [ (Blast_tac 1) ]);
   12.64 +Goalw [domain_def] "a: domain(r) <-> (EX y. <a,y>: r)";
   12.65 +by (Blast_tac 1) ;
   12.66 +qed "domain_iff";
   12.67  
   12.68  Goal "<a,b>: r ==> a: domain(r)";
   12.69  by (etac (exI RS (domain_iff RS iffD2)) 1) ;
   12.70 @@ -82,44 +82,48 @@
   12.71  
   12.72  (*** range ***)
   12.73  
   12.74 -qed_goalw "rangeI" thy [range_def] "!!a b r.<a,b>: r ==> b : range(r)"
   12.75 - (fn _ => [ (etac (converseI RS domainI) 1) ]);
   12.76 +Goalw [range_def]  "<a,b>: r ==> b : range(r)";
   12.77 +by (etac (converseI RS domainI) 1) ;
   12.78 +qed "rangeI";
   12.79  
   12.80 -qed_goalw "rangeE" thy [range_def]
   12.81 -    "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P"
   12.82 - (fn major::prems=>
   12.83 -  [ (rtac (major RS domainE) 1),
   12.84 -    (resolve_tac prems 1),
   12.85 -    (etac converseD 1) ]);
   12.86 +val major::prems= Goalw [range_def] 
   12.87 +    "[| b : range(r);  !!x. <x,b>: r ==> P |] ==> P";
   12.88 +by (rtac (major RS domainE) 1);
   12.89 +by (resolve_tac prems 1);
   12.90 +by (etac converseD 1) ;
   12.91 +qed "rangeE";
   12.92  
   12.93  AddIs  [rangeI];
   12.94  AddSEs [rangeE];
   12.95  
   12.96 -qed_goalw "range_subset" thy [range_def] "range(A*B) <= B"
   12.97 - (fn _ =>
   12.98 -  [ (stac converse_prod 1),
   12.99 -    (rtac domain_subset 1) ]);
  12.100 +Goalw [range_def]  "range(A*B) <= B";
  12.101 +by (stac converse_prod 1);
  12.102 +by (rtac domain_subset 1) ;
  12.103 +qed "range_subset";
  12.104  
  12.105  
  12.106  (*** field ***)
  12.107  
  12.108 -qed_goalw "fieldI1" thy [field_def] "!!r. <a,b>: r ==> a : field(r)"
  12.109 - (fn _ => [ (Blast_tac 1) ]);
  12.110 -
  12.111 -qed_goalw "fieldI2" thy [field_def] "!!r. <a,b>: r ==> b : field(r)"
  12.112 - (fn _ => [ (Blast_tac 1) ]);
  12.113 +Goalw [field_def]  "<a,b>: r ==> a : field(r)";
  12.114 +by (Blast_tac 1) ;
  12.115 +qed "fieldI1";
  12.116  
  12.117 -qed_goalw "fieldCI" thy [field_def]
  12.118 -    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
  12.119 - (fn [prem]=> [ (blast_tac (claset() addIs [prem]) 1) ]);
  12.120 +Goalw [field_def]  "<a,b>: r ==> b : field(r)";
  12.121 +by (Blast_tac 1) ;
  12.122 +qed "fieldI2";
  12.123  
  12.124 -qed_goalw "fieldE" thy [field_def]
  12.125 +val [prem]= Goalw [field_def] 
  12.126 +    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
  12.127 +by (blast_tac (claset() addIs [prem]) 1) ;
  12.128 +qed "fieldCI";
  12.129 +
  12.130 +val major::prems= Goalw [field_def] 
  12.131       "[| a : field(r);  \
  12.132  \        !!x. <a,x>: r ==> P;  \
  12.133 -\        !!x. <x,a>: r ==> P        |] ==> P"
  12.134 - (fn major::prems=>
  12.135 -  [ (rtac (major RS UnE) 1),
  12.136 -    (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
  12.137 +\        !!x. <x,a>: r ==> P        |] ==> P";
  12.138 +by (rtac (major RS UnE) 1);
  12.139 +by (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ;
  12.140 +qed "fieldE";
  12.141  
  12.142  AddIs  [fieldCI];
  12.143  AddSEs [fieldE];
  12.144 @@ -128,13 +132,13 @@
  12.145  by (Blast_tac 1) ;
  12.146  qed "field_subset";
  12.147  
  12.148 -qed_goalw "domain_subset_field" thy [field_def]
  12.149 -    "domain(r) <= field(r)"
  12.150 - (fn _ => [ (rtac Un_upper1 1) ]);
  12.151 +Goalw [field_def] "domain(r) <= field(r)";
  12.152 +by (rtac Un_upper1 1) ;
  12.153 +qed "domain_subset_field";
  12.154  
  12.155 -qed_goalw "range_subset_field" thy [field_def]
  12.156 -    "range(r) <= field(r)"
  12.157 - (fn _ => [ (rtac Un_upper2 1) ]);
  12.158 +Goalw [field_def] "range(r) <= field(r)";
  12.159 +by (rtac Un_upper2 1) ;
  12.160 +qed "range_subset_field";
  12.161  
  12.162  Goal "r <= Sigma(A,B) ==> r <= domain(r)*range(r)";
  12.163  by (Blast_tac 1) ;
  12.164 @@ -156,15 +160,15 @@
  12.165  by (Blast_tac 1) ;
  12.166  qed "image_singleton_iff";
  12.167  
  12.168 -qed_goalw "imageI" thy [image_def]
  12.169 -    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r``A"
  12.170 - (fn _ => [ (Blast_tac 1) ]);
  12.171 +Goalw [image_def] "[| <a,b>: r;  a:A |] ==> b : r``A";
  12.172 +by (Blast_tac 1) ;
  12.173 +qed "imageI";
  12.174  
  12.175 -qed_goalw "imageE" thy [image_def]
  12.176 -    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
  12.177 - (fn major::prems=>
  12.178 -  [ (rtac (major RS CollectE) 1),
  12.179 -    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
  12.180 +val major::prems= Goalw [image_def] 
  12.181 +    "[| b: r``A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P";
  12.182 +by (rtac (major RS CollectE) 1);
  12.183 +by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
  12.184 +qed "imageE";
  12.185  
  12.186  AddIs  [imageI];
  12.187  AddSEs [imageE];
  12.188 @@ -176,28 +180,29 @@
  12.189  
  12.190  (*** Inverse image of a set under a function/relation ***)
  12.191  
  12.192 -qed_goalw "vimage_iff" thy [vimage_def,image_def,converse_def]
  12.193 -    "a : r-``B <-> (EX y:B. <a,y>:r)"
  12.194 - (fn _ => [ (Blast_tac 1) ]);
  12.195 +Goalw [vimage_def,image_def,converse_def] 
  12.196 +    "a : r-``B <-> (EX y:B. <a,y>:r)";
  12.197 +by (Blast_tac 1) ;
  12.198 +qed "vimage_iff";
  12.199  
  12.200  Goal "a : r-``{b} <-> <a,b>:r";
  12.201  by (rtac (vimage_iff RS iff_trans) 1);
  12.202  by (Blast_tac 1) ;
  12.203  qed "vimage_singleton_iff";
  12.204  
  12.205 -qed_goalw "vimageI" thy [vimage_def]
  12.206 -    "!!A B r. [| <a,b>: r;  b:B |] ==> a : r-``B"
  12.207 - (fn _ => [ (Blast_tac 1) ]);
  12.208 +Goalw [vimage_def] "[| <a,b>: r;  b:B |] ==> a : r-``B";
  12.209 +by (Blast_tac 1) ;
  12.210 +qed "vimageI";
  12.211  
  12.212 -qed_goalw "vimageE" thy [vimage_def]
  12.213 -    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P"
  12.214 - (fn major::prems=>
  12.215 -  [ (rtac (major RS imageE) 1),
  12.216 -    (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ]);
  12.217 +val major::prems= Goalw [vimage_def] 
  12.218 +    "[| a: r-``B;  !!x.[| <a,x>: r;  x:B |] ==> P |] ==> P";
  12.219 +by (rtac (major RS imageE) 1);
  12.220 +by (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ;
  12.221 +qed "vimageE";
  12.222  
  12.223 -qed_goalw "vimage_subset" thy [vimage_def]
  12.224 -    "!!A B r. r <= A*B ==> r-``C <= A"
  12.225 - (fn _ => [ (etac (converse_type RS image_subset) 1) ]);
  12.226 +Goalw [vimage_def] "r <= A*B ==> r-``C <= A";
  12.227 +by (etac (converse_type RS image_subset) 1) ;
  12.228 +qed "vimage_subset";
  12.229  
  12.230  
  12.231  (** Theorem-proving for ZF set theory **)
    13.1 --- a/src/ZF/func.ML	Fri Jun 30 12:49:11 2000 +0200
    13.2 +++ b/src/ZF/func.ML	Fri Jun 30 12:51:30 2000 +0200
    13.3 @@ -237,13 +237,16 @@
    13.4  qed "fun_extension_iff";
    13.5  
    13.6  (*thanks to Mark Staples*)
    13.7 -val fun_subset_eq = prove_goal thy
    13.8 -    "!!f. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
    13.9 - (fn _=> 
   13.10 -  [ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2),
   13.11 -    (rtac fun_extension 1), (REPEAT (atac 1)),
   13.12 -    (dtac (apply_Pair RSN (2,subsetD)) 1), (REPEAT (atac 1)),
   13.13 -    (rtac (apply_equality RS sym) 1), (REPEAT (atac 1)) ]);
   13.14 +Goal "[| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)";
   13.15 +by (rtac iffI 1);
   13.16 +by (asm_full_simp_tac ZF_ss 2);
   13.17 +by (rtac fun_extension 1);
   13.18 +by (REPEAT (atac 1));
   13.19 +by (dtac (apply_Pair RSN (2,subsetD)) 1);
   13.20 +by (REPEAT (atac 1));
   13.21 +by (rtac (apply_equality RS sym) 1);
   13.22 +by (REPEAT (atac 1)) ;
   13.23 +qed "fun_subset_eq";
   13.24  
   13.25  
   13.26  (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
    14.1 --- a/src/ZF/pair.ML	Fri Jun 30 12:49:11 2000 +0200
    14.2 +++ b/src/ZF/pair.ML	Fri Jun 30 12:51:30 2000 +0200
    14.3 @@ -18,10 +18,10 @@
    14.4  by (Blast_tac 1) ;
    14.5  qed "doubleton_eq_iff";
    14.6  
    14.7 -qed_goalw "Pair_iff" thy [Pair_def]
    14.8 -    "<a,b> = <c,d> <-> a=c & b=d"
    14.9 - (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1),
   14.10 -           (Blast_tac 1) ]);
   14.11 +Goalw [Pair_def] "<a,b> = <c,d> <-> a=c & b=d";
   14.12 +by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1);
   14.13 +by (Blast_tac 1) ;
   14.14 +qed "Pair_iff";
   14.15  
   14.16  Addsimps [Pair_iff];
   14.17  
   14.18 @@ -32,31 +32,33 @@
   14.19  bind_thm ("Pair_inject1", Pair_iff RS iffD1 RS conjunct1);
   14.20  bind_thm ("Pair_inject2", Pair_iff RS iffD1 RS conjunct2);
   14.21  
   14.22 -qed_goalw "Pair_not_0" thy [Pair_def] "<a,b> ~= 0"
   14.23 - (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
   14.24 +Goalw [Pair_def]  "<a,b> ~= 0";
   14.25 +by (blast_tac (claset() addEs [equalityE]) 1) ;
   14.26 +qed "Pair_not_0";
   14.27  
   14.28  bind_thm ("Pair_neq_0", Pair_not_0 RS notE);
   14.29  
   14.30  AddSEs [Pair_neq_0, sym RS Pair_neq_0];
   14.31  
   14.32 -qed_goalw "Pair_neq_fst" thy [Pair_def] "<a,b>=a ==> P"
   14.33 - (fn [major]=>
   14.34 -  [ (rtac (consI1 RS mem_asym RS FalseE) 1),
   14.35 -    (rtac (major RS subst) 1),
   14.36 -    (rtac consI1 1) ]);
   14.37 +Goalw [Pair_def]  "<a,b>=a ==> P";
   14.38 +by (rtac (consI1 RS mem_asym RS FalseE) 1);
   14.39 +by (etac subst 1);
   14.40 +by (rtac consI1 1) ;
   14.41 +qed "Pair_neq_fst";
   14.42  
   14.43 -qed_goalw "Pair_neq_snd" thy [Pair_def] "<a,b>=b ==> P"
   14.44 - (fn [major]=>
   14.45 -  [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
   14.46 -    (rtac (major RS subst) 1),
   14.47 -    (rtac (consI1 RS consI2) 1) ]);
   14.48 +Goalw [Pair_def]  "<a,b>=b ==> P";
   14.49 +by (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1);
   14.50 +by (etac subst 1);
   14.51 +by (rtac (consI1 RS consI2) 1) ;
   14.52 +qed "Pair_neq_snd";
   14.53  
   14.54  
   14.55  (*** Sigma: Disjoint union of a family of sets
   14.56       Generalizes Cartesian product ***)
   14.57  
   14.58 -qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
   14.59 - (fn _ => [ Blast_tac 1 ]);
   14.60 +Goalw [Sigma_def]  "<a,b>: Sigma(A,B) <-> a:A & b:B(a)";
   14.61 +by (Blast_tac 1) ;
   14.62 +qed "Sigma_iff";
   14.63  
   14.64  Addsimps [Sigma_iff];
   14.65  
   14.66 @@ -70,13 +72,13 @@
   14.67  bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2);
   14.68  
   14.69  (*The general elimination rule*)
   14.70 -qed_goalw "SigmaE" thy [Sigma_def]
   14.71 +val major::prems= Goalw [Sigma_def] 
   14.72      "[| c: Sigma(A,B);  \
   14.73  \       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
   14.74 -\    |] ==> P"
   14.75 - (fn major::prems=>
   14.76 -  [ (cut_facts_tac [major] 1),
   14.77 -    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
   14.78 +\    |] ==> P";
   14.79 +by (cut_facts_tac [major] 1);
   14.80 +by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
   14.81 +qed "SigmaE";
   14.82  
   14.83  val [major,minor]= Goal
   14.84      "[| <a,b> : Sigma(A,B);    \
   14.85 @@ -87,10 +89,11 @@
   14.86  by (rtac (major RS SigmaD2) 1) ;
   14.87  qed "SigmaE2";
   14.88  
   14.89 -qed_goalw "Sigma_cong" thy [Sigma_def]
   14.90 +val prems= Goalw [Sigma_def] 
   14.91      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
   14.92 -\    Sigma(A,B) = Sigma(A',B')"
   14.93 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
   14.94 +\    Sigma(A,B) = Sigma(A',B')";
   14.95 +by (simp_tac (simpset() addsimps prems) 1) ;
   14.96 +qed "Sigma_cong";
   14.97  
   14.98  
   14.99  (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
  14.100 @@ -117,11 +120,13 @@
  14.101  
  14.102  (*** Projections: fst, snd ***)
  14.103  
  14.104 -qed_goalw "fst_conv" thy [fst_def] "fst(<a,b>) = a"
  14.105 - (fn _=> [ (Blast_tac 1) ]);
  14.106 +Goalw [fst_def]  "fst(<a,b>) = a";
  14.107 +by (Blast_tac 1) ;
  14.108 +qed "fst_conv";
  14.109  
  14.110 -qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b"
  14.111 - (fn _=> [ (Blast_tac 1) ]);
  14.112 +Goalw [snd_def]  "snd(<a,b>) = b";
  14.113 +by (Blast_tac 1) ;
  14.114 +qed "snd_conv";
  14.115  
  14.116  Addsimps [fst_conv,snd_conv];
  14.117  
    15.1 --- a/src/ZF/subset.ML	Fri Jun 30 12:49:11 2000 +0200
    15.2 +++ b/src/ZF/subset.ML	Fri Jun 30 12:51:30 2000 +0200
    15.3 @@ -41,16 +41,16 @@
    15.4  
    15.5  (*But if j is an ordinal or is transitive, then i:j implies i<=j! 
    15.6    See ordinal/Ord_succ_subsetI*)
    15.7 -qed_goalw "succ_subsetI" thy [succ_def]
    15.8 -    "!!i j. [| i:j;  i<=j |] ==> succ(i)<=j"
    15.9 - (fn _=> [ (Blast_tac 1) ]);
   15.10 +Goalw [succ_def] "[| i:j;  i<=j |] ==> succ(i)<=j";
   15.11 +by (Blast_tac 1) ;
   15.12 +qed "succ_subsetI";
   15.13  
   15.14 -qed_goalw "succ_subsetE" thy [succ_def] 
   15.15 +val major::prems= Goalw [succ_def]  
   15.16      "[| succ(i) <= j;  [| i:j;  i<=j |] ==> P \
   15.17 -\    |] ==> P"
   15.18 - (fn major::prems=>
   15.19 -  [ (rtac (major RS cons_subsetE) 1),
   15.20 -    (REPEAT (ares_tac prems 1)) ]);
   15.21 +\    |] ==> P";
   15.22 +by (rtac (major RS cons_subsetE) 1);
   15.23 +by (REPEAT (ares_tac prems 1)) ;
   15.24 +qed "succ_subsetE";
   15.25  
   15.26  (*** singletons ***)
   15.27  
    16.1 --- a/src/ZF/upair.ML	Fri Jun 30 12:49:11 2000 +0200
    16.2 +++ b/src/ZF/upair.ML	Fri Jun 30 12:51:30 2000 +0200
    16.3 @@ -20,9 +20,9 @@
    16.4  
    16.5  (*** Unordered pairs - Upair ***)
    16.6  
    16.7 -qed_goalw "Upair_iff" thy [Upair_def]
    16.8 -    "c : Upair(a,b) <-> (c=a | c=b)"
    16.9 - (fn _ => [ (Blast_tac 1) ]);
   16.10 +Goalw [Upair_def] "c : Upair(a,b) <-> (c=a | c=b)";
   16.11 +by (Blast_tac 1) ;
   16.12 +qed "Upair_iff";
   16.13  
   16.14  Addsimps [Upair_iff];
   16.15  
   16.16 @@ -45,8 +45,9 @@
   16.17  
   16.18  (*** Rules for binary union -- Un -- defined via Upair ***)
   16.19  
   16.20 -qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
   16.21 - (fn _ => [(Blast_tac 1)]);
   16.22 +Goalw [Un_def]  "c : A Un B <-> (c:A | c:B)";
   16.23 +by (Blast_tac 1);
   16.24 +qed "Un_iff";
   16.25  
   16.26  Addsimps [Un_iff];
   16.27  
   16.28 @@ -87,8 +88,9 @@
   16.29  
   16.30  (*** Rules for small intersection -- Int -- defined via Upair ***)
   16.31  
   16.32 -qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
   16.33 - (fn _ => [(Blast_tac 1)]);
   16.34 +Goalw [Int_def]  "c : A Int B <-> (c:A & c:B)";
   16.35 +by (Blast_tac 1);
   16.36 +qed "Int_iff";
   16.37  
   16.38  Addsimps [Int_iff];
   16.39  
   16.40 @@ -114,8 +116,9 @@
   16.41  
   16.42  (*** Rules for set difference -- defined via Upair ***)
   16.43  
   16.44 -qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
   16.45 - (fn _ => [(Blast_tac 1)]);
   16.46 +Goalw [Diff_def]  "c : A-B <-> (c:A & c~:B)";
   16.47 +by (Blast_tac 1);
   16.48 +qed "Diff_iff";
   16.49  
   16.50  Addsimps [Diff_iff];
   16.51  
   16.52 @@ -141,8 +144,9 @@
   16.53  
   16.54  (*** Rules for cons -- defined via Un and Upair ***)
   16.55  
   16.56 -qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
   16.57 - (fn _ => [(Blast_tac 1)]);
   16.58 +Goalw [cons_def]  "a : cons(b,A) <-> (a=b | a:A)";
   16.59 +by (Blast_tac 1);
   16.60 +qed "cons_iff";
   16.61  
   16.62  Addsimps [cons_iff];
   16.63  
   16.64 @@ -210,10 +214,10 @@
   16.65  
   16.66  (*** Rules for Descriptions ***)
   16.67  
   16.68 -qed_goalw "the_equality" thy [the_def]
   16.69 -    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
   16.70 - (fn [pa,eq] =>
   16.71 -  [ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]);
   16.72 +val [pa,eq] = Goalw [the_def] 
   16.73 +    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a";
   16.74 +by (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ;
   16.75 +qed "the_equality";
   16.76  
   16.77  AddIs [the_equality];
   16.78  
   16.79 @@ -337,23 +341,25 @@
   16.80  
   16.81  (*** Rules for succ ***)
   16.82  
   16.83 -qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
   16.84 - (fn _ => [(Blast_tac 1)]);
   16.85 +Goalw [succ_def]  "i : succ(j) <-> i=j | i:j";
   16.86 +by (Blast_tac 1);
   16.87 +qed "succ_iff";
   16.88  
   16.89 -qed_goalw "succI1" thy [succ_def] "i : succ(i)"
   16.90 - (fn _=> [ (rtac consI1 1) ]);
   16.91 +Goalw [succ_def]  "i : succ(i)";
   16.92 +by (rtac consI1 1) ;
   16.93 +qed "succI1";
   16.94  
   16.95  Addsimps [succI1];
   16.96  
   16.97 -qed_goalw "succI2" thy [succ_def]
   16.98 -    "i : j ==> i : succ(j)"
   16.99 - (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
  16.100 +Goalw [succ_def] "i : j ==> i : succ(j)";
  16.101 +by (etac consI2 1) ;
  16.102 +qed "succI2";
  16.103  
  16.104 -qed_goalw "succE" thy [succ_def]
  16.105 -    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
  16.106 - (fn major::prems=>
  16.107 -  [ (rtac (major RS consE) 1),
  16.108 -    (REPEAT (eresolve_tac prems 1)) ]);
  16.109 +val major::prems= Goalw [succ_def] 
  16.110 +    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P";
  16.111 +by (rtac (major RS consE) 1);
  16.112 +by (REPEAT (eresolve_tac prems 1)) ;
  16.113 +qed "succE";
  16.114  
  16.115  (*Classical introduction rule*)
  16.116  val [prem]= Goal "(i~:j ==> i=j) ==> i: succ(j)";