# HG changeset patch
# User lcp
# Date 771870745 -7200
# Node ID 3410f4d8508679304fac16179ff4132c41bfb8a7
# Parent  e886a3010f8b6d3f75425c7ca478584e73f979fa
HOL/HOL.ML/notE: tidied the proof

diff -r e886a3010f8b -r 3410f4d85086 HOL.ML
--- 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]);