--- 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 *)