--- a/HOL.ML Fri Jun 17 18:30:18 1994 +0200
+++ b/HOL.ML Fri Jun 17 18:32:25 1994 +0200
@@ -155,8 +155,8 @@
(** 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, fold_tac [False_def], resolve_tac prems 1]);
+val FalseE = prove_goalw HOL.thy [False_def] "False ==> P"
+ (fn [major] => [rtac (major RS spec) 1]);
val False_neq_True = prove_goal HOL.thy "False=True ==> P"
(fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);