diff -r c801110efa1b -r 722bf1319be5 HOL.ML
--- a/HOL.ML	Mon Oct 31 17:17:48 1994 +0100
+++ b/HOL.ML	Tue Nov 01 11:00:45 1994 +0100
@@ -60,7 +60,6 @@
   val ssubst	: thm
   val stac	: thm -> int -> tactic
   val strip_tac	: int -> tactic
-  val swap	: thm
   val sym	: thm
   val trans	: thm
   val TrueI	: thm
@@ -230,26 +229,17 @@
 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 a1 1,
-	 rtac (a2 RS impI) 1, atac 1, rtac (a3 RS impI) 1, atac 1]);
+	 rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 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, fold_tac [False_def], resolve_tac prems 1,
-    rtac ssubst 1, atac 1, rewtac not_def,
-    REPEAT (ares_tac [impI] 1) ]);
+val classical = prove_goalw HOL.thy [not_def]  "(~P ==> P) ==> P"
+ (fn [prem] =>
+   [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
+    rtac (impI RS prem RS eqTrueI) 1,
+    etac subst 1,  assume_tac 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)]);
-
+val ccontr = FalseE RS classical;
 
 (*Double negation law*)
 val notnotD = prove_goal HOL.thy "~~P ==> P"
@@ -319,10 +309,6 @@
   [ (rtac ccontr 1),
     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
 
-(*Required by the "classical" module*)
-val swap = prove_goal HOL.thy "~P ==> (~Q ==> P) ==> Q"
- (fn major::prems=>
-  [ rtac ccontr 1, rtac (major RS notE) 1, REPEAT (ares_tac prems 1)]);
 
 (* case distinction *)