# HG changeset patch
# User clasohm
# Date 790527921 -3600
# Node ID 2d3d020eef1168446c17d56a1114a6424ecc935b
# Parent  b38c67991122e785c98188b82414c49c89fe9431
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
and theory_of_thm

diff -r b38c67991122 -r 2d3d020eef11 doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Wed Jan 18 11:36:04 1995 +0100
+++ b/doc-src/Ref/defining.tex	Thu Jan 19 16:05:21 1995 +0100
@@ -688,26 +688,10 @@
 {\out ...}
 \end{ttbox}
 
-On the other hand it's also possible that none of the parse trees can be
-typed correctly although the user did not make a mistake.
-
-%% FIXME remove?
-%By default Isabelle
-%assumes that the type of a syntax translation rule is {\tt logic} but does
-%not look at the type unless parsing the rule produces more than one parse
-%tree. In that case this message is output if the rule's type is different
-%from {\tt logic}:
-%
-%\begin{ttbox}
-%{\out Warning: Ambiguous input "..."}
-%{\out produces the following parse trees:}
-%{\out ...}
-%{\out This occured in syntax translation rule: "..."  ->  "..."}
-%{\out Type checking error: Term does not have expected type}
-%{\out ...}
-%\end{ttbox}
-%
-%To circumvent this the rule's type has to be stated.
+Ambiguities occuring in syntax translation rules cannot be resolved by
+type inference because it is not necessary for these rules to be type
+correct. Therefore Isabelle always generates an error message and the
+ambiguity should be eliminated by changing the grammar or the rule.
 
 
 \section{Example: some minimal logics} \label{sec:min_logics}
diff -r b38c67991122 -r 2d3d020eef11 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Wed Jan 18 11:36:04 1995 +0100
+++ b/doc-src/Ref/goals.tex	Thu Jan 19 16:05:21 1995 +0100
@@ -117,34 +117,47 @@
   the goal in intuitionistic logic and proving it using classical logic.
 \end{itemize}
 
-\subsection{Extracting the proved theorem}
+\subsection{Extracting and storing the proved theorem}
+\label{ExtractingAndStoringTheProvedTheorem}
 \index{theorems!from subgoal module}
 \begin{ttbox} 
-result  : unit -> thm
-uresult : unit -> thm
+result    : unit -> thm
+uresult   : unit -> thm
+bind_thm  : string * thm -> unit
+qed       : string -> unit
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{result}()]\index{assumptions!of main goal}
-returns the final theorem, after converting the free variables to
-schematics.  It discharges the assumptions supplied to the matching 
-{\tt goal} command.  
+  returns the final theorem, after converting the free variables to
+  schematics.  It discharges the assumptions supplied to the matching 
+  {\tt goal} command.  
 
-It raises an exception unless the proof state passes certain checks.  There
-must be no assumptions other than those supplied to {\tt goal}.  There
-must be no subgoals.  The theorem proved must be a (first-order) instance
-of the original goal, as stated in the {\tt goal} command.  This allows
-{\bf answer extraction} --- instantiation of variables --- but no other
-changes to the main goal.  The theorem proved must have the same signature
-as the initial proof state.
+  It raises an exception unless the proof state passes certain checks.  There
+  must be no assumptions other than those supplied to {\tt goal}.  There
+  must be no subgoals.  The theorem proved must be a (first-order) instance
+  of the original goal, as stated in the {\tt goal} command.  This allows
+  {\bf answer extraction} --- instantiation of variables --- but no other
+  changes to the main goal.  The theorem proved must have the same signature
+  as the initial proof state.
 
-These checks are needed because an Isabelle tactic can return any proof
-state at all.
+  These checks are needed because an Isabelle tactic can return any proof
+  state at all.
 
 \item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.
   It is needed when the initial goal contains function unknowns, when
   definitions are unfolded in the main goal (by calling
   \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
   \ttindex{assume_ax} has been used.
+
+\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
+  stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
+  in Isabelle's theorem database and in the ML variable $name$. The
+  theorem can be retrieved from Isabelle's database by {\tt get_thm}
+  (see \S\ref{BasicOperationsOnTheories}).
+
+\item[\ttindexbold{qed} $name$]
+  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
+  result()} to get the theorem and then stores it like {\tt bind_thm}.
 \end{ttdescription}
 
 
@@ -332,8 +345,10 @@
 \section{Executing batch proofs}
 \index{batch execution}
 \begin{ttbox}
-prove_goal  :  theory->          string->(thm list->tactic list)->thm
-prove_goalw :  theory->thm list->string->(thm list->tactic list)->thm
+prove_goal :         theory->          string->(thm list->tactic list)->thm
+qed_goal   : string->theory->          string->(thm list->tactic list)->unit
+prove_goalw:         theory->thm list->string->(thm list->tactic list)->thm
+qed_goalw  : string->theory->thm list->string->(thm list->tactic list)->unit
 prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
 \end{ttbox}
 These batch functions create an initial proof state, then apply a tactic to
@@ -366,11 +381,19 @@
 executes a proof of the {\it formula\/} in the given {\it theory}, using
 the given tactic function.
 
+\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
+acts like {\tt prove_goal} but also stores the resulting theorem in
+Isabelle's theorem database and in the ML variable $name$ (see
+\S\ref{ExtractingAndStoringTheProvedTheorem}).
+
 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
       {\it tacsf};]\index{meta-rewriting}
 is like {\tt prove_goal} but also applies the list of {\it defs\/} as
 meta-rewrite rules to the first subgoal and the premises.
 
+\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
+is analogous to {\tt qed_goal}.
+
 \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
       {\it tacsf};] 
 is a version of {\tt prove_goalw} for programming applications.  The main
diff -r b38c67991122 -r 2d3d020eef11 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Wed Jan 18 11:36:04 1995 +0100
+++ b/doc-src/Ref/theories.tex	Thu Jan 19 16:05:21 1995 +0100
@@ -308,7 +308,7 @@
 
 
 
-\section{Basic operations on theories}
+\section{Basic operations on theories}\label{BasicOperationsOnTheories}
 \subsection{Extracting an axiom or theorem from a theory}
 \index{theories!axioms of}\index{axioms!extracting}
 \index{theories!theorems of}\index{theorems!extracting}
@@ -319,12 +319,14 @@
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{get_axiom} $thy$ $name$]
-returns an axiom with the given $name$ from $thy$, raising exception
-\xdx{THEORY} if none exists.  Merging theories can cause several axioms
-to have the same name; {\tt get_axiom} returns an arbitrary one.
+  returns an axiom with the given $name$ from $thy$, raising exception
+  \xdx{THEORY} if none exists.  Merging theories can cause several axioms
+  to have the same name; {\tt get_axiom} returns an arbitrary one.
 
 \item[\ttindexbold{get_thm} $thy$ $name$]
-  is analogous to {\tt get_axiom}, but looks for a stored theorem.
+  is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
+  {\tt get_axiom} it searches all parents of a theory if the theorem
+  is not associated with $thy$.
 
 \item[\ttindexbold{assume_ax} $thy$ $formula$]
   reads the {\it formula} using the syntax of $thy$, following the same
@@ -427,7 +429,7 @@
 returns the additional axioms of the most recent extend node of~$thy$.
 
 \item[\ttindexbold{thms_of} $thy$]
-similar to {\tt axioms_of}, but returns the stored theorems.
+returns all theorems that are associated with $thy$.
 
 \item[\ttindexbold{parents_of} $thy$]
 returns the direct ancestors of~$thy$.
diff -r b38c67991122 -r 2d3d020eef11 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Wed Jan 18 11:36:04 1995 +0100
+++ b/doc-src/Ref/thm.tex	Thu Jan 19 16:05:21 1995 +0100
@@ -166,7 +166,7 @@
 \end{ttdescription}
 
 
-\subsection{Miscellaneous forward rules}
+\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
 \index{theorems!standardizing}
 \begin{ttbox} 
 standard         :           thm -> thm
@@ -209,6 +209,7 @@
 nprems_of     : thm -> int
 tpairs_of     : thm -> (term*term)list
 stamps_of_thy : thm -> string ref list
+theory_of_thm : thm -> theory
 dest_state    : thm*int -> (term*term)list*term list*term*term
 rep_thm       : thm -> \{prop:term, hyps:term list, 
                         maxidx:int, sign:Sign.sg\}
@@ -230,6 +231,9 @@
 \item[\ttindexbold{stamps_of_thm} $thm$] 
 returns the \rmindex{stamps} of the signature associated with~$thm$.
 
+\item[\ttindexbold{theory_of_thm} $thm$]
+returns the theory associated with $thm$.
+
 \item[\ttindexbold{dest_state} $(thm,i)$] 
 decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
 list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem