# HG changeset patch
# User wenzelm
# Date 1003090021 -7200
# Node ID 1fcf1eb516084b805f80f08fa3600ff9b0058807
# Parent  48bc55f4377461fb6b20daf44dce90900bcc593e
added qed_spec_mp etc.;

diff -r 48bc55f43774 -r 1fcf1eb51608 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Sun Oct 14 22:05:46 2001 +0200
+++ b/src/Pure/Thy/thm_database.ML	Sun Oct 14 22:07:01 2001 +0200
@@ -14,6 +14,10 @@
   val qed: string -> unit
   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
   val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit
+  val qed_spec_mp: string -> unit
+  val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit
+  val qed_goalw_spec_mp: string -> theory -> thm list -> string
+    -> (thm list -> tactic list) -> unit
   val no_qed: unit -> unit
   (*these peek at the proof state!*)
   val thms_containing: xstring list -> (string * thm) list
@@ -89,6 +93,11 @@
 fun qed name = ml_store_thm (name, Goals.result ());
 fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
 fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
+fun qed_spec_mp name = ml_store_thm (name, ObjectLogic.rulify_no_asm (Goals.result ()));
+fun qed_goal_spec_mp name thy s p =
+  bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
+fun qed_goalw_spec_mp name thy defs s p =
+  bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
 
 fun no_qed () = ();