hol.ML

     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
 
 (** 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)]);
 
 val eqTrueE = prove_goal HOL.thy "P=True ==> P" 
  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
 
 (** 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 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 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_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=>
   [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
 

 
 (** False ** Depends upon spec; it is impossible to do propositional logic
              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]);
 
 
 (** 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 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 notI = prove_goalw HOL.thy [not_def] "(P ==> False) ==> ~P"
+ (fn prems=> [rtac impI 1, eresolve_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 **)
 
 val impE = prove_goal HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);

 val [not_sym] = compose(sym,2,contrapos);
 
 
 (** 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 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 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_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"
- (fn prems =>
-  [ (rtac (and_def RS ssubst) 1), 
-    (REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)) ]);
-
-val conjunct1 = prove_goal HOL.thy "[| P & Q |] ==> P"
- (fn prems =>
-   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
-     (REPEAT(ares_tac [impI] 1)) ]);
-
-val conjunct2 = prove_goal HOL.thy "[| P & Q |] ==> Q" 
- (fn prems =>
-   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
-     (REPEAT(ares_tac [impI] 1)) ]);
+val conjI = prove_goalw HOL.thy [and_def] "[| P; Q |] ==> P&Q"
+ (fn prems =>
+  [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
+
+val conjunct1 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> P"
+ (fn prems =>
+   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
+
+val conjunct2 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> Q"
+ (fn prems =>
+   [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 =>
 	 [cut_facts_tac prems 1, resolve_tac prems 1,
 	  etac conjunct1 1, etac conjunct2 1]);
 
 (** 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 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 disjE = prove_goal HOL.thy "[| P | Q; P ==> R; Q ==> R |] ==> R"
+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_goalw HOL.thy [or_def] "Q ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+
+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 **)
 
 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 ccontr = prove_goalw HOL.thy [not_def] "(~P ==> False) ==> P"
+ (fn prems =>
+   [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)]);
+ (fn prems => [rtac ccontr 1, REPEAT (ares_tac (prems@[notE]) 1)]);
 
 
 (*Double negation law*)
 val notnotD = prove_goal HOL.thy "~~P ==> P"
  (fn [major]=>
   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
 
 
 (** 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)) ]);
-
-val ex1E = prove_goal HOL.thy
+  [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
+
+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 **)
 
 val select_equality = prove_goal HOL.thy