# HG changeset patch
# User clasohm
# Date 785751229 -3600
# Node ID 6e815617d79fd6ae6b1a3b68287bad9a04f4de68
# Parent  45a78940780641d0719ae449939ca8a1888a2a4d
added qed_goal[w]

diff -r 45a789407806 -r 6e815617d79f src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Nov 25 00:02:37 1994 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Nov 25 09:13:49 1994 +0100
@@ -40,6 +40,10 @@
   val theory_of_thm: thm -> theory
   val store_thm: string * thm -> thm
   val qed: string -> unit
+  val qed_goal_thm: thm ref
+  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 get_thm: theory -> string -> thm
   val thms_of: theory -> (string * thm) list
 end;
@@ -490,6 +494,16 @@
 fun qed name =
   use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"];
 
+val qed_goal_thm = ref flexpair_def(*dummy*);
+fun qed_goal name thy agoal tacsf =
+  (qed_goal_thm := prove_goal thy agoal tacsf;
+   use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ 
+               ", !qed_goal_thm);"]);
+
+fun qed_goalw name thy rths agoal tacsf =
+  (qed_goal_thm := prove_goalw thy rths agoal tacsf;
+   use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ 
+               ", !qed_goal_thm);"]);
 
 (* Retrieve theorems *)