--- a/doc-src/Ref/goals.tex Fri Sep 03 10:14:28 1999 +0200
+++ b/doc-src/Ref/goals.tex Fri Sep 03 13:55:46 1999 +0200
@@ -135,6 +135,7 @@
\index{theorems!extracting proved}
\begin{ttbox}
qed : string -> unit
+no_qed : unit -> unit
result : unit -> thm
uresult : unit -> thm
bind_thm : string * thm -> unit
@@ -147,6 +148,11 @@
It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem
using \texttt{result()} and stores it the theorem database associated
with its theory. See below for details.
+
+\item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a
+ proper \texttt{qed} command. This is a do-nothing operation, it merely
+ helps user interfaces such as Proof~General \cite{proofgeneral} to figure
+ out the structure of the {\ML} text.
\item[\ttindexbold{result}()]\index{assumptions!of main goal}
returns the final theorem, after converting the free variables to
--- a/src/Pure/Thy/thm_database.ML Fri Sep 03 10:14:28 1999 +0200
+++ b/src/Pure/Thy/thm_database.ML Fri Sep 03 13:55:46 1999 +0200
@@ -14,6 +14,7 @@
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 no_qed: unit -> unit
(*these peek at the proof state!*)
val thms_containing: xstring list -> (string * thm) list
val findI: int -> (string * thm) list
@@ -79,10 +80,13 @@
fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
fun bind_thms (name, thms) = ml_store_thms (name, map standard thms);
+
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 no_qed () = ();
+
(** retrieve theorems **)