# HG changeset patch
# User wenzelm
# Date 1028842969 -7200
# Node ID 7123ae179212f23a661420b31c98b41ed7bd4ec8
# Parent  9cfbcb9acfefda39c81b62c06eb56d3f9192a66c
Tactic.prove, Tactic.prove_standard;

diff -r 9cfbcb9acfef -r 7123ae179212 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Thu Aug 08 23:42:10 2002 +0200
+++ b/doc-src/Ref/goals.tex	Thu Aug 08 23:42:49 2002 +0200
@@ -549,6 +549,34 @@
 \end{ttdescription}
 
 
+\section{Internal proofs}
+
+\begin{ttbox}
+Tactic.prove: Sign.sg -> string list -> term list -> term ->
+  (thm list -> tactic) -> thm
+Tactic.prove_standard: Sign.sg -> string list -> term list -> term ->
+  (thm list -> tactic) -> thm
+\end{ttbox}
+
+These functions provide a clean internal interface for programmed proofs.  The
+special overhead of top-level statements (cf.\ \verb,prove_goalw_cterm,) is
+omitted.  Statements may be established within a local contexts of fixed
+variables and assumptions, which are the only hypotheses to be discharged in
+the result.
+
+\begin{ttdescription}
+\item[\ttindexbold{Tactic.prove}~$sg~xs~As~C~tacf$] establishes the result
+  $\Forall xs. As \Imp C$ via the given tactic (which is a function taking the
+  assumptions as local premises).
+  
+\item[\ttindexbold{Tactic.prove_standard}] is simular to \verb,Tactic.prove,,
+  but performs the \verb,standard, operation on the result, essentially
+  turning it into a top-level statement.  Never do this for local proofs
+  within other proof tools!
+
+\end{ttdescription}
+
+
 \section{Managing multiple proofs}
 \index{proofs!managing multiple}
 You may save the current state of the subgoal module and resume work on it