1.1 --- a/doc-src/Ref/goals.tex	Wed Jan 18 11:36:04 1995 +0100
     1.2 +++ b/doc-src/Ref/goals.tex	Thu Jan 19 16:05:21 1995 +0100
     1.3 @@ -117,34 +117,47 @@
     1.4    the goal in intuitionistic logic and proving it using classical logic.
     1.5  \end{itemize}
     1.6  
     1.7 -\subsection{Extracting the proved theorem}
     1.8 +\subsection{Extracting and storing the proved theorem}
     1.9 +\label{ExtractingAndStoringTheProvedTheorem}
    1.10  \index{theorems!from subgoal module}
    1.11  \begin{ttbox} 
    1.12 -result  : unit -> thm
    1.13 -uresult : unit -> thm
    1.14 +result    : unit -> thm
    1.15 +uresult   : unit -> thm
    1.16 +bind_thm  : string * thm -> unit
    1.17 +qed       : string -> unit
    1.18  \end{ttbox}
    1.19  \begin{ttdescription}
    1.20  \item[\ttindexbold{result}()]\index{assumptions!of main goal}
    1.21 -returns the final theorem, after converting the free variables to
    1.22 -schematics.  It discharges the assumptions supplied to the matching 
    1.23 -{\tt goal} command.  
    1.24 +  returns the final theorem, after converting the free variables to
    1.25 +  schematics.  It discharges the assumptions supplied to the matching 
    1.26 +  {\tt goal} command.  
    1.27  
    1.28 -It raises an exception unless the proof state passes certain checks.  There
    1.29 -must be no assumptions other than those supplied to {\tt goal}.  There
    1.30 -must be no subgoals.  The theorem proved must be a (first-order) instance
    1.31 -of the original goal, as stated in the {\tt goal} command.  This allows
    1.32 -{\bf answer extraction} --- instantiation of variables --- but no other
    1.33 -changes to the main goal.  The theorem proved must have the same signature
    1.34 -as the initial proof state.
    1.35 +  It raises an exception unless the proof state passes certain checks.  There
    1.36 +  must be no assumptions other than those supplied to {\tt goal}.  There
    1.37 +  must be no subgoals.  The theorem proved must be a (first-order) instance
    1.38 +  of the original goal, as stated in the {\tt goal} command.  This allows
    1.39 +  {\bf answer extraction} --- instantiation of variables --- but no other
    1.40 +  changes to the main goal.  The theorem proved must have the same signature
    1.41 +  as the initial proof state.
    1.42  
    1.43 -These checks are needed because an Isabelle tactic can return any proof
    1.44 -state at all.
    1.45 +  These checks are needed because an Isabelle tactic can return any proof
    1.46 +  state at all.
    1.47  
    1.48  \item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.
    1.49    It is needed when the initial goal contains function unknowns, when
    1.50    definitions are unfolded in the main goal (by calling
    1.51    \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
    1.52    \ttindex{assume_ax} has been used.
    1.53 +
    1.54 +\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
    1.55 +  stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
    1.56 +  in Isabelle's theorem database and in the ML variable $name$. The
    1.57 +  theorem can be retrieved from Isabelle's database by {\tt get_thm}
    1.58 +  (see \S\ref{BasicOperationsOnTheories}).
    1.59 +
    1.60 +\item[\ttindexbold{qed} $name$]
    1.61 +  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
    1.62 +  result()} to get the theorem and then stores it like {\tt bind_thm}.
    1.63  \end{ttdescription}
    1.64  
    1.65  
    1.66 @@ -332,8 +345,10 @@
    1.67  \section{Executing batch proofs}
    1.68  \index{batch execution}
    1.69  \begin{ttbox}
    1.70 -prove_goal  :  theory->          string->(thm list->tactic list)->thm
    1.71 -prove_goalw :  theory->thm list->string->(thm list->tactic list)->thm
    1.72 +prove_goal :         theory->          string->(thm list->tactic list)->thm
    1.73 +qed_goal   : string->theory->          string->(thm list->tactic list)->unit
    1.74 +prove_goalw:         theory->thm list->string->(thm list->tactic list)->thm
    1.75 +qed_goalw  : string->theory->thm list->string->(thm list->tactic list)->unit
    1.76  prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
    1.77  \end{ttbox}
    1.78  These batch functions create an initial proof state, then apply a tactic to
    1.79 @@ -366,11 +381,19 @@
    1.80  executes a proof of the {\it formula\/} in the given {\it theory}, using
    1.81  the given tactic function.
    1.82  
    1.83 +\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
    1.84 +acts like {\tt prove_goal} but also stores the resulting theorem in
    1.85 +Isabelle's theorem database and in the ML variable $name$ (see
    1.86 +\S\ref{ExtractingAndStoringTheProvedTheorem}).
    1.87 +
    1.88  \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
    1.89        {\it tacsf};]\index{meta-rewriting}
    1.90  is like {\tt prove_goal} but also applies the list of {\it defs\/} as
    1.91  meta-rewrite rules to the first subgoal and the premises.
    1.92  
    1.93 +\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
    1.94 +is analogous to {\tt qed_goal}.
    1.95 +
    1.96  \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
    1.97        {\it tacsf};] 
    1.98  is a version of {\tt prove_goalw} for programming applications.  The main