# HG changeset patch
# User nipkow
# Date 766745400 -7200
# Node ID 14b9286ed036f116542a04ac9a8bb9a259d75c92
# Parent  52771c21d9ca299f4b45b17548c9ca18aaf2c525
changed defns in hol.thy from = to ==

diff -r 52771c21d9ca -r 14b9286ed036 HOL.ML
--- a/HOL.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/HOL.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -125,7 +125,8 @@
 
 (** True **)
 
-val TrueI = refl RS (True_def RS iffD2);
+val TrueI = prove_goalw HOL.thy [True_def] "True"
+  (fn _ => [rtac refl 1]);
 
 val eqTrueI  = prove_goal HOL.thy "P ==> P=True" 
  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
@@ -135,13 +136,11 @@
 
 (** Universal quantifier **)
 
-val allI = prove_goal HOL.thy "(!!x::'a. P(x)) ==> !x. P(x)"
- (fn [asm] => [rtac (All_def RS ssubst) 1, rtac (asm RS (eqTrueI RS ext)) 1]);
+val allI = prove_goalw HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
+ (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
 
-val spec = prove_goal HOL.thy "! x::'a.P(x) ==> P(x)"
- (fn prems =>
-   [ rtac eqTrueE 1, 
-     resolve_tac (prems RL [All_def RS subst] RL [fun_cong]) 1 ]);
+val spec = prove_goalw HOL.thy [All_def] "! x::'a.P(x) ==> P(x)"
+ (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
 
 val allE = prove_goal HOL.thy "[| !x.P(x);  P(x) ==> R |] ==> R"
  (fn major::prems=>
@@ -157,7 +156,7 @@
              before quantifiers! **)
 
 val FalseE = prove_goal HOL.thy "False ==> P"
- (fn prems => [rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1]);
+ (fn prems => [rtac spec 1, fold_tac [False_def], resolve_tac prems 1]);
 
 val False_neq_True = prove_goal HOL.thy "False=True ==> P"
  (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
@@ -165,14 +164,11 @@
 
 (** Negation **)
 
-val notI = prove_goal HOL.thy  "(P ==> False) ==> ~P"
- (fn prems=> [rtac (not_def RS ssubst) 1, rtac impI 1, eresolve_tac prems 1]);
+val notI = prove_goalw HOL.thy [not_def] "(P ==> False) ==> ~P"
+ (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
 
-val notE = prove_goal HOL.thy "[| ~P;  P |] ==> R"
- (fn prems =>
-    [rtac (mp RS FalseE) 1, 
-     resolve_tac prems 2, rtac (not_def RS subst) 1,
-     resolve_tac prems 1]);
+val notE = prove_goalw HOL.thy [not_def] "[| ~P;  P |] ==> R"
+ (fn prems => [rtac (mp RS FalseE) 1, REPEAT(resolve_tac prems 1)]);
 
 (** Implication **)
 
@@ -194,33 +190,27 @@
 
 (** Existential quantifier **)
 
-val exI = prove_goal HOL.thy "P(x) ==> ? x::'a.P(x)"
- (fn prems =>
-	[rtac (selectI RS (Ex_def RS ssubst)) 1,
-	 resolve_tac prems 1]);
+val exI = prove_goalw HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
+ (fn prems => [rtac selectI 1, resolve_tac prems 1]);
 
-val exE = prove_goal HOL.thy "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
-	(fn prems =>
-	[resolve_tac prems 1, res_inst_tac [("P","%C.C(P)")] subst 1,
-	 rtac Ex_def 1, resolve_tac prems 1]);
+val exE = prove_goalw HOL.thy [Ex_def]
+  "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+  (fn prems => [REPEAT(resolve_tac prems 1)]);
 
 
 (** Conjunction **)
 
-val conjI = prove_goal HOL.thy "[| P; Q |] ==> P&Q"
+val conjI = prove_goalw HOL.thy [and_def] "[| P; Q |] ==> P&Q"
  (fn prems =>
-  [ (rtac (and_def RS ssubst) 1), 
-    (REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)) ]);
+  [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
 
-val conjunct1 = prove_goal HOL.thy "[| P & Q |] ==> P"
+val conjunct1 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> P"
  (fn prems =>
-   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
-     (REPEAT(ares_tac [impI] 1)) ]);
+   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
 
-val conjunct2 = prove_goal HOL.thy "[| P & Q |] ==> Q" 
+val conjunct2 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> Q"
  (fn prems =>
-   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
-     (REPEAT(ares_tac [impI] 1)) ]);
+   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
 
 val conjE = prove_goal HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
  (fn prems =>
@@ -229,19 +219,15 @@
 
 (** Disjunction *)
 
-val disjI1 = prove_goal HOL.thy "P ==> P|Q"
- (fn [prem] =>
-	[rtac (or_def RS ssubst) 1,
-	 REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI1 = prove_goalw HOL.thy [or_def] "P ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
 
-val disjI2 = prove_goal HOL.thy "Q ==> P|Q"
- (fn [prem] =>
-	[rtac (or_def RS ssubst) 1,
-	 REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI2 = prove_goalw HOL.thy [or_def] "Q ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
 
-val disjE = prove_goal HOL.thy "[| P | Q; P ==> R; Q ==> R |] ==> R"
+val disjE = prove_goalw HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
  (fn [a1,a2,a3] =>
-	[rtac (mp RS mp) 1, rtac spec 1, rtac (or_def RS subst) 1, rtac a1 1,
+	[rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
 	 rtac (a2 RS impI) 1, atac 1, rtac (a3 RS impI) 1, atac 1]);
 
 (** CCONTR -- classical logic **)
@@ -249,14 +235,18 @@
 val ccontr = prove_goal HOL.thy "(~P ==> False) ==> P"
  (fn prems =>
    [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
-    rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1,
-    rtac ssubst 1, atac 1, rtac (not_def RS ssubst) 1,
+    rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+    rtac ssubst 1, atac 1, rewtac not_def,
     REPEAT (ares_tac [impI] 1) ]);
 
-val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+val ccontr = prove_goalw HOL.thy [not_def] "(~P ==> False) ==> P"
  (fn prems =>
-   [rtac ccontr 1,
-    REPEAT (ares_tac (prems@[notE]) 1)]);
+   [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
+    rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+    rtac ssubst 1, atac 1, REPEAT (ares_tac [impI] 1) ]);
+
+val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+ (fn prems => [rtac ccontr 1, REPEAT (ares_tac (prems@[notE]) 1)]);
 
 
 (*Double negation law*)
@@ -267,17 +257,15 @@
 
 (** Unique existence **)
 
-val ex1I = prove_goal HOL.thy
+val ex1I = prove_goalw HOL.thy [Ex1_def]
     "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
  (fn prems =>
-  [ (rtac (Ex1_def RS ssubst) 1),
-    (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
+  [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
 
-val ex1E = prove_goal HOL.thy
+val ex1E = prove_goalw HOL.thy [Ex1_def]
     "[| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
  (fn major::prems =>
-  [ (resolve_tac ([major] RL [Ex1_def RS subst] RL [exE]) 1),
-    (REPEAT (etac conjE 1 ORELSE ares_tac prems 1)) ]);
+  [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
 
 
 (** Select: Hilbert's Epsilon-operator **)
diff -r 52771c21d9ca -r 14b9286ed036 HOL.thy
--- a/HOL.thy	Wed Apr 06 16:31:06 1994 +0200
+++ b/HOL.thy	Tue Apr 19 10:50:00 1994 +0200
@@ -103,15 +103,15 @@
 
   (* Definitions *)
 
-  True_def      "True = ((%x::bool.x)=(%x.x))"
-  All_def       "All  = (%P. P = (%x.True))"
-  Ex_def        "Ex   = (%P. P(@x.P(x)))"
-  False_def     "False = (!P.P)"
-  not_def       "not  = (%P. P-->False)"
-  and_def       "op & = (%P Q. !R. (P-->Q-->R) --> R)"
-  or_def        "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
-  Ex1_def       "Ex1  = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
-  Let_def       "Let(s, f) = f(s)"
+  True_def      "True == ((%x::bool.x)=(%x.x))"
+  All_def       "All  == (%P. P = (%x.True))"
+  Ex_def        "Ex   == (%P. P(@x.P(x)))"
+  False_def     "False == (!P.P)"
+  not_def       "not  == (%P. P-->False)"
+  and_def       "op & == (%P Q. !R. (P-->Q-->R) --> R)"
+  or_def        "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+  Ex1_def       "Ex1  == (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+  Let_def       "Let(s, f) == f(s)"
 
   (* Axioms *)
 
@@ -120,10 +120,10 @@
 
   (* Misc Definitions *)
 
-  Inv_def       "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
-  o_def         "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+  Inv_def       "Inv == (%(f::'a=>'b) y. @x. f(x)=y)"
+  o_def         "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))"
 
-  if_def        "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+  if_def        "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
 
 end
 
diff -r 52771c21d9ca -r 14b9286ed036 LList.ML
--- a/LList.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/LList.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -483,10 +483,9 @@
 
 (** Two easy results about Lmap **)
 
-val [prem] = goal LList.thy
+val [prem] = goalw LList.thy [o_def]
     "M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
 by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (stac o_def 1);
 by (safe_tac set_cs);
 by (etac LListE 1);
 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
diff -r 52771c21d9ca -r 14b9286ed036 Univ.ML
--- a/Univ.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/Univ.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -147,16 +147,14 @@
 val inj_Atom = result();
 val Atom_inject = inj_Atom RS injD;
 
-goalw Univ.thy [Leaf_def] "inj(Leaf)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inl_inject) 1);
 val inj_Leaf = result();
 
 val Leaf_inject = inj_Leaf RS injD;
 
-goalw Univ.thy [Numb_def] "inj(Numb)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inr_inject) 1);
 val inj_Numb = result();
@@ -223,8 +221,7 @@
 
 (** Scons vs Leaf **)
 
-goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
 by (rtac Scons_not_Atom 1);
 val Scons_not_Leaf = result();
 val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
@@ -234,8 +231,7 @@
 
 (** Scons vs Numb **)
 
-goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
 by (rtac Scons_not_Atom 1);
 val Scons_not_Numb = result();
 val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
@@ -301,13 +297,11 @@
 by (rtac zero_less_Suc 1);
 val ntrunc_Atom = result();
 
-goalw Univ.thy [Leaf_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
 by (rtac ntrunc_Atom 1);
 val ntrunc_Leaf = result();
 
-goalw Univ.thy [Numb_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
 by (rtac ntrunc_Atom 1);
 val ntrunc_Numb = result();
 
@@ -432,10 +426,10 @@
 by (rtac (major RS equalityD2) 1);
 val ntrunc_equality = result();
 
-val [major] = goal Univ.thy
+val [major] = goalw Univ.thy [o_def]
     "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
-by (resolve_tac ([major RS fun_cong] RL [o_def RS subst]) 1);
+by (rtac (major RS fun_cong) 1);
 val ntrunc_o_equality = result();
 
 (*** Monotonicity ***)
diff -r 52771c21d9ca -r 14b9286ed036 ex/PL.ML
--- a/ex/PL.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/ex/PL.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -174,8 +174,8 @@
 val [major] = goalw PL.thy [sat_def] "H |- p ==> H |= p";
 by (rtac (major RS conseq_induct) 1);
 by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (asm_simp_tac(pl_ss addsimps
-                [ball_eq,not_def RS fun_cong RS sym])));
+by (ALLGOALS (asm_simp_tac(pl_ss addsimps [ball_eq])));
+by(fast_tac HOL_cs 1);
 val soundness = result();
 
 (** Structural induction on pl
@@ -261,8 +261,7 @@
 goal PL.thy "hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
 by (PL0.induct_tac "p" 1);
 by (simp_tac pl_ss 1);
-by (simp_tac (pl_ss addsimps [insert_subset]
-                    setloop (split_tac [expand_if])) 1);
+by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
 by (simp_tac pl_ss 1);
 by (fast_tac set_cs 1);
 val hyps_insert = result();
diff -r 52771c21d9ca -r 14b9286ed036 ex/pl.ML
--- a/ex/pl.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/ex/pl.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -174,8 +174,8 @@
 val [major] = goalw PL.thy [sat_def] "H |- p ==> H |= p";
 by (rtac (major RS conseq_induct) 1);
 by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (asm_simp_tac(pl_ss addsimps
-                [ball_eq,not_def RS fun_cong RS sym])));
+by (ALLGOALS (asm_simp_tac(pl_ss addsimps [ball_eq])));
+by(fast_tac HOL_cs 1);
 val soundness = result();
 
 (** Structural induction on pl
@@ -261,8 +261,7 @@
 goal PL.thy "hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
 by (PL0.induct_tac "p" 1);
 by (simp_tac pl_ss 1);
-by (simp_tac (pl_ss addsimps [insert_subset]
-                    setloop (split_tac [expand_if])) 1);
+by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
 by (simp_tac pl_ss 1);
 by (fast_tac set_cs 1);
 val hyps_insert = result();
diff -r 52771c21d9ca -r 14b9286ed036 fun.ML
--- a/fun.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/fun.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -49,8 +49,7 @@
 by (REPEAT (ares_tac prems 1));
 val imageE = result();
 
-goal Set.thy "(f o g)``r = f``(g``r)";
-by (stac o_def 1);
+goalw Set.thy [o_def] "(f o g)``r = f``(g``r)";
 by (rtac set_ext 1);
 by (fast_tac (HOL_cs addIs [imageI] addSEs [imageE]) 1);
 val image_compose = result();
@@ -94,8 +93,8 @@
 val inj_select = result();
 
 (*A one-to-one function has an inverse (given using select).*)
-val [major] = goal Set.thy "inj(f) ==> Inv(f,f(x)) = x";
-by (EVERY1 [stac Inv_def, rtac (major RS inj_select)]);
+val [major] = goalw Set.thy [Inv_def] "inj(f) ==> Inv(f,f(x)) = x";
+by (EVERY1 [rtac (major RS inj_select)]);
 val Inv_f_f = result();
 
 (* Useful??? *)
@@ -136,9 +135,8 @@
 
 (*** Lemmas about inj ***)
 
-val prems = goal Set.thy
+val prems = goalw Set.thy [o_def]
     "[| inj(f);  inj_onto(g,range(f)) |] ==> inj(g o f)";
-by (stac o_def 1);
 by (cut_facts_tac prems 1);
 by (fast_tac (HOL_cs addIs [injI,rangeI]
                      addEs [injD,inj_ontoD]) 1);
@@ -148,8 +146,8 @@
 by (fast_tac (HOL_cs addIs [prem RS injD, inj_ontoI]) 1);
 val inj_imp = result();
 
-val [prem] = goal Set.thy "y : range(f) ==> f(Inv(f,y)) = y";
-by (EVERY1 [stac Inv_def, rtac (prem RS rangeE), rtac selectI, etac sym]);
+val [prem] = goalw Set.thy [Inv_def] "y : range(f) ==> f(Inv(f,y)) = y";
+by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
 val f_Inv_f = result();
 
 val prems = goal Set.thy
diff -r 52771c21d9ca -r 14b9286ed036 hol.ML
--- a/hol.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/hol.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -125,7 +125,8 @@
 
 (** True **)
 
-val TrueI = refl RS (True_def RS iffD2);
+val TrueI = prove_goalw HOL.thy [True_def] "True"
+  (fn _ => [rtac refl 1]);
 
 val eqTrueI  = prove_goal HOL.thy "P ==> P=True" 
  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
@@ -135,13 +136,11 @@
 
 (** Universal quantifier **)
 
-val allI = prove_goal HOL.thy "(!!x::'a. P(x)) ==> !x. P(x)"
- (fn [asm] => [rtac (All_def RS ssubst) 1, rtac (asm RS (eqTrueI RS ext)) 1]);
+val allI = prove_goalw HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
+ (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
 
-val spec = prove_goal HOL.thy "! x::'a.P(x) ==> P(x)"
- (fn prems =>
-   [ rtac eqTrueE 1, 
-     resolve_tac (prems RL [All_def RS subst] RL [fun_cong]) 1 ]);
+val spec = prove_goalw HOL.thy [All_def] "! x::'a.P(x) ==> P(x)"
+ (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
 
 val allE = prove_goal HOL.thy "[| !x.P(x);  P(x) ==> R |] ==> R"
  (fn major::prems=>
@@ -157,7 +156,7 @@
              before quantifiers! **)
 
 val FalseE = prove_goal HOL.thy "False ==> P"
- (fn prems => [rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1]);
+ (fn prems => [rtac spec 1, fold_tac [False_def], resolve_tac prems 1]);
 
 val False_neq_True = prove_goal HOL.thy "False=True ==> P"
  (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
@@ -165,14 +164,11 @@
 
 (** Negation **)
 
-val notI = prove_goal HOL.thy  "(P ==> False) ==> ~P"
- (fn prems=> [rtac (not_def RS ssubst) 1, rtac impI 1, eresolve_tac prems 1]);
+val notI = prove_goalw HOL.thy [not_def] "(P ==> False) ==> ~P"
+ (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
 
-val notE = prove_goal HOL.thy "[| ~P;  P |] ==> R"
- (fn prems =>
-    [rtac (mp RS FalseE) 1, 
-     resolve_tac prems 2, rtac (not_def RS subst) 1,
-     resolve_tac prems 1]);
+val notE = prove_goalw HOL.thy [not_def] "[| ~P;  P |] ==> R"
+ (fn prems => [rtac (mp RS FalseE) 1, REPEAT(resolve_tac prems 1)]);
 
 (** Implication **)
 
@@ -194,33 +190,27 @@
 
 (** Existential quantifier **)
 
-val exI = prove_goal HOL.thy "P(x) ==> ? x::'a.P(x)"
- (fn prems =>
-	[rtac (selectI RS (Ex_def RS ssubst)) 1,
-	 resolve_tac prems 1]);
+val exI = prove_goalw HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
+ (fn prems => [rtac selectI 1, resolve_tac prems 1]);
 
-val exE = prove_goal HOL.thy "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
-	(fn prems =>
-	[resolve_tac prems 1, res_inst_tac [("P","%C.C(P)")] subst 1,
-	 rtac Ex_def 1, resolve_tac prems 1]);
+val exE = prove_goalw HOL.thy [Ex_def]
+  "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+  (fn prems => [REPEAT(resolve_tac prems 1)]);
 
 
 (** Conjunction **)
 
-val conjI = prove_goal HOL.thy "[| P; Q |] ==> P&Q"
+val conjI = prove_goalw HOL.thy [and_def] "[| P; Q |] ==> P&Q"
  (fn prems =>
-  [ (rtac (and_def RS ssubst) 1), 
-    (REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)) ]);
+  [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
 
-val conjunct1 = prove_goal HOL.thy "[| P & Q |] ==> P"
+val conjunct1 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> P"
  (fn prems =>
-   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
-     (REPEAT(ares_tac [impI] 1)) ]);
+   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
 
-val conjunct2 = prove_goal HOL.thy "[| P & Q |] ==> Q" 
+val conjunct2 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> Q"
  (fn prems =>
-   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
-     (REPEAT(ares_tac [impI] 1)) ]);
+   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
 
 val conjE = prove_goal HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
  (fn prems =>
@@ -229,19 +219,15 @@
 
 (** Disjunction *)
 
-val disjI1 = prove_goal HOL.thy "P ==> P|Q"
- (fn [prem] =>
-	[rtac (or_def RS ssubst) 1,
-	 REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI1 = prove_goalw HOL.thy [or_def] "P ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
 
-val disjI2 = prove_goal HOL.thy "Q ==> P|Q"
- (fn [prem] =>
-	[rtac (or_def RS ssubst) 1,
-	 REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI2 = prove_goalw HOL.thy [or_def] "Q ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
 
-val disjE = prove_goal HOL.thy "[| P | Q; P ==> R; Q ==> R |] ==> R"
+val disjE = prove_goalw HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
  (fn [a1,a2,a3] =>
-	[rtac (mp RS mp) 1, rtac spec 1, rtac (or_def RS subst) 1, rtac a1 1,
+	[rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
 	 rtac (a2 RS impI) 1, atac 1, rtac (a3 RS impI) 1, atac 1]);
 
 (** CCONTR -- classical logic **)
@@ -249,14 +235,18 @@
 val ccontr = prove_goal HOL.thy "(~P ==> False) ==> P"
  (fn prems =>
    [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
-    rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1,
-    rtac ssubst 1, atac 1, rtac (not_def RS ssubst) 1,
+    rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+    rtac ssubst 1, atac 1, rewtac not_def,
     REPEAT (ares_tac [impI] 1) ]);
 
-val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+val ccontr = prove_goalw HOL.thy [not_def] "(~P ==> False) ==> P"
  (fn prems =>
-   [rtac ccontr 1,
-    REPEAT (ares_tac (prems@[notE]) 1)]);
+   [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
+    rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+    rtac ssubst 1, atac 1, REPEAT (ares_tac [impI] 1) ]);
+
+val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+ (fn prems => [rtac ccontr 1, REPEAT (ares_tac (prems@[notE]) 1)]);
 
 
 (*Double negation law*)
@@ -267,17 +257,15 @@
 
 (** Unique existence **)
 
-val ex1I = prove_goal HOL.thy
+val ex1I = prove_goalw HOL.thy [Ex1_def]
     "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
  (fn prems =>
-  [ (rtac (Ex1_def RS ssubst) 1),
-    (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
+  [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
 
-val ex1E = prove_goal HOL.thy
+val ex1E = prove_goalw HOL.thy [Ex1_def]
     "[| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
  (fn major::prems =>
-  [ (resolve_tac ([major] RL [Ex1_def RS subst] RL [exE]) 1),
-    (REPEAT (etac conjE 1 ORELSE ares_tac prems 1)) ]);
+  [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
 
 
 (** Select: Hilbert's Epsilon-operator **)
diff -r 52771c21d9ca -r 14b9286ed036 hol.thy
--- a/hol.thy	Wed Apr 06 16:31:06 1994 +0200
+++ b/hol.thy	Tue Apr 19 10:50:00 1994 +0200
@@ -103,15 +103,15 @@
 
   (* Definitions *)
 
-  True_def      "True = ((%x::bool.x)=(%x.x))"
-  All_def       "All  = (%P. P = (%x.True))"
-  Ex_def        "Ex   = (%P. P(@x.P(x)))"
-  False_def     "False = (!P.P)"
-  not_def       "not  = (%P. P-->False)"
-  and_def       "op & = (%P Q. !R. (P-->Q-->R) --> R)"
-  or_def        "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
-  Ex1_def       "Ex1  = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
-  Let_def       "Let(s, f) = f(s)"
+  True_def      "True == ((%x::bool.x)=(%x.x))"
+  All_def       "All  == (%P. P = (%x.True))"
+  Ex_def        "Ex   == (%P. P(@x.P(x)))"
+  False_def     "False == (!P.P)"
+  not_def       "not  == (%P. P-->False)"
+  and_def       "op & == (%P Q. !R. (P-->Q-->R) --> R)"
+  or_def        "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+  Ex1_def       "Ex1  == (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+  Let_def       "Let(s, f) == f(s)"
 
   (* Axioms *)
 
@@ -120,10 +120,10 @@
 
   (* Misc Definitions *)
 
-  Inv_def       "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
-  o_def         "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+  Inv_def       "Inv == (%(f::'a=>'b) y. @x. f(x)=y)"
+  o_def         "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))"
 
-  if_def        "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+  if_def        "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
 
 end
 
diff -r 52771c21d9ca -r 14b9286ed036 llist.ML
--- a/llist.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/llist.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -483,10 +483,9 @@
 
 (** Two easy results about Lmap **)
 
-val [prem] = goal LList.thy
+val [prem] = goalw LList.thy [o_def]
     "M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
 by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (stac o_def 1);
 by (safe_tac set_cs);
 by (etac LListE 1);
 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
diff -r 52771c21d9ca -r 14b9286ed036 simpdata.ML
--- a/simpdata.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/simpdata.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -46,8 +46,8 @@
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
 	(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
 
-val o_apply = prove_goal HOL.thy "(f o g)(x) = f(g(x))"
- (fn _ => [ (stac o_def 1), (rtac refl 1) ]);
+val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
+ (fn _ => [rtac refl 1]);
 
 val simp_thms = map prover
  [ "(x=x) = True",
@@ -73,11 +73,11 @@
 val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
 val conj_comms = [conj_commute, conj_left_commute];
 
-val if_True = prove_goal HOL.thy "if(True,x,y) = x"
- (fn _=>[stac if_def 1,  fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
 
-val if_False = prove_goal HOL.thy "if(False,x,y) = y"
- (fn _=>[stac if_def 1,  fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
 
 val if_P = prove_goal HOL.thy "P ==> if(P,x,y) = x"
  (fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -112,7 +112,7 @@
   let val lemma1 = prove_goal HOL.thy
         "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
         (fn prems => [resolve_tac prems 1, etac exI 1]);
-      val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+      val lemma2 = prove_goalw HOL.thy [Ex_def]
         "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
         (fn prems => [REPEAT(resolve_tac prems 1)])
   in equal_intr lemma1 lemma2 end;
diff -r 52771c21d9ca -r 14b9286ed036 univ.ML
--- a/univ.ML	Wed Apr 06 16:31:06 1994 +0200
+++ b/univ.ML	Tue Apr 19 10:50:00 1994 +0200
@@ -147,16 +147,14 @@
 val inj_Atom = result();
 val Atom_inject = inj_Atom RS injD;
 
-goalw Univ.thy [Leaf_def] "inj(Leaf)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inl_inject) 1);
 val inj_Leaf = result();
 
 val Leaf_inject = inj_Leaf RS injD;
 
-goalw Univ.thy [Numb_def] "inj(Numb)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
 by (rtac injI 1);
 by (etac (Atom_inject RS Inr_inject) 1);
 val inj_Numb = result();
@@ -223,8 +221,7 @@
 
 (** Scons vs Leaf **)
 
-goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
 by (rtac Scons_not_Atom 1);
 val Scons_not_Leaf = result();
 val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
@@ -234,8 +231,7 @@
 
 (** Scons vs Numb **)
 
-goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
 by (rtac Scons_not_Atom 1);
 val Scons_not_Numb = result();
 val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
@@ -301,13 +297,11 @@
 by (rtac zero_less_Suc 1);
 val ntrunc_Atom = result();
 
-goalw Univ.thy [Leaf_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
 by (rtac ntrunc_Atom 1);
 val ntrunc_Leaf = result();
 
-goalw Univ.thy [Numb_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
 by (rtac ntrunc_Atom 1);
 val ntrunc_Numb = result();
 
@@ -432,10 +426,10 @@
 by (rtac (major RS equalityD2) 1);
 val ntrunc_equality = result();
 
-val [major] = goal Univ.thy
+val [major] = goalw Univ.thy [o_def]
     "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
-by (resolve_tac ([major RS fun_cong] RL [o_def RS subst]) 1);
+by (rtac (major RS fun_cong) 1);
 val ntrunc_o_equality = result();
 
 (*** Monotonicity ***)