# HG changeset patch
# User oheimb
# Date 850918267 -3600
# Node ID 6663e0d210b0d0cd179e37c1a453001336828d1e
# Parent  decc46a5cdb58145176418af4dd8a365f33e96cd
added qed_goal_spec_mp and qed_goalw_spec_mp

diff -r decc46a5cdb5 -r 6663e0d210b0 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Dec 18 15:10:33 1996 +0100
+++ b/src/HOL/HOL.ML	Wed Dec 18 15:11:07 1996 +0100
@@ -123,6 +123,8 @@
 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
 
+bind_thm ("classical2", notE RS notI);
+
 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
  (fn _ => [REPEAT (ares_tac [notE] 1)]);
 
@@ -344,6 +346,12 @@
   let val thm = normalize_thm [RSspec,RSmp] (result())
   in bind_thm(name, thm) end;
 
+fun qed_goal_spec_mp name thy s p = 
+	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
+
+fun qed_goalw_spec_mp name thy defs s p = 
+	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
+
 end;