# HG changeset patch
# User wenzelm
# Date 936359746 -7200
# Node ID f43d3670a3cd07ee0c7a652af4debf9686c593c3
# Parent  6dd6110968c9e5007c25a44b194c42844fc02f54
added no_qed;

diff -r 6dd6110968c9 -r f43d3670a3cd doc-src/Ref/goals.tex
--- 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
diff -r 6dd6110968c9 -r f43d3670a3cd src/Pure/Thy/thm_database.ML
--- 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 **)