1.1 --- a/doc-src/Ref/defining.tex	Wed Jan 18 11:36:04 1995 +0100
     1.2 +++ b/doc-src/Ref/defining.tex	Thu Jan 19 16:05:21 1995 +0100
     1.3 @@ -688,26 +688,10 @@
     1.4  {\out ...}
     1.5  \end{ttbox}
     1.6  
     1.7 -On the other hand it's also possible that none of the parse trees can be
     1.8 -typed correctly although the user did not make a mistake.
     1.9 -
    1.10 -%% FIXME remove?
    1.11 -%By default Isabelle
    1.12 -%assumes that the type of a syntax translation rule is {\tt logic} but does
    1.13 -%not look at the type unless parsing the rule produces more than one parse
    1.14 -%tree. In that case this message is output if the rule's type is different
    1.15 -%from {\tt logic}:
    1.16 -%
    1.17 -%\begin{ttbox}
    1.18 -%{\out Warning: Ambiguous input "..."}
    1.19 -%{\out produces the following parse trees:}
    1.20 -%{\out ...}
    1.21 -%{\out This occured in syntax translation rule: "..."  ->  "..."}
    1.22 -%{\out Type checking error: Term does not have expected type}
    1.23 -%{\out ...}
    1.24 -%\end{ttbox}
    1.25 -%
    1.26 -%To circumvent this the rule's type has to be stated.
    1.27 +Ambiguities occuring in syntax translation rules cannot be resolved by
    1.28 +type inference because it is not necessary for these rules to be type
    1.29 +correct. Therefore Isabelle always generates an error message and the
    1.30 +ambiguity should be eliminated by changing the grammar or the rule.
    1.31  
    1.32  
    1.33  \section{Example: some minimal logics} \label{sec:min_logics}

     2.1 --- a/doc-src/Ref/goals.tex	Wed Jan 18 11:36:04 1995 +0100
     2.2 +++ b/doc-src/Ref/goals.tex	Thu Jan 19 16:05:21 1995 +0100
     2.3 @@ -117,34 +117,47 @@
     2.4    the goal in intuitionistic logic and proving it using classical logic.
     2.5  \end{itemize}
     2.6  
     2.7 -\subsection{Extracting the proved theorem}
     2.8 +\subsection{Extracting and storing the proved theorem}
     2.9 +\label{ExtractingAndStoringTheProvedTheorem}
    2.10  \index{theorems!from subgoal module}
    2.11  \begin{ttbox} 
    2.12 -result  : unit -> thm
    2.13 -uresult : unit -> thm
    2.14 +result    : unit -> thm
    2.15 +uresult   : unit -> thm
    2.16 +bind_thm  : string * thm -> unit
    2.17 +qed       : string -> unit
    2.18  \end{ttbox}
    2.19  \begin{ttdescription}
    2.20  \item[\ttindexbold{result}()]\index{assumptions!of main goal}
    2.21 -returns the final theorem, after converting the free variables to
    2.22 -schematics.  It discharges the assumptions supplied to the matching 
    2.23 -{\tt goal} command.  
    2.24 +  returns the final theorem, after converting the free variables to
    2.25 +  schematics.  It discharges the assumptions supplied to the matching 
    2.26 +  {\tt goal} command.  
    2.27  
    2.28 -It raises an exception unless the proof state passes certain checks.  There
    2.29 -must be no assumptions other than those supplied to {\tt goal}.  There
    2.30 -must be no subgoals.  The theorem proved must be a (first-order) instance
    2.31 -of the original goal, as stated in the {\tt goal} command.  This allows
    2.32 -{\bf answer extraction} --- instantiation of variables --- but no other
    2.33 -changes to the main goal.  The theorem proved must have the same signature
    2.34 -as the initial proof state.
    2.35 +  It raises an exception unless the proof state passes certain checks.  There
    2.36 +  must be no assumptions other than those supplied to {\tt goal}.  There
    2.37 +  must be no subgoals.  The theorem proved must be a (first-order) instance
    2.38 +  of the original goal, as stated in the {\tt goal} command.  This allows
    2.39 +  {\bf answer extraction} --- instantiation of variables --- but no other
    2.40 +  changes to the main goal.  The theorem proved must have the same signature
    2.41 +  as the initial proof state.
    2.42  
    2.43 -These checks are needed because an Isabelle tactic can return any proof
    2.44 -state at all.
    2.45 +  These checks are needed because an Isabelle tactic can return any proof
    2.46 +  state at all.
    2.47  
    2.48  \item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.
    2.49    It is needed when the initial goal contains function unknowns, when
    2.50    definitions are unfolded in the main goal (by calling
    2.51    \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
    2.52    \ttindex{assume_ax} has been used.
    2.53 +
    2.54 +\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
    2.55 +  stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
    2.56 +  in Isabelle's theorem database and in the ML variable $name$. The
    2.57 +  theorem can be retrieved from Isabelle's database by {\tt get_thm}
    2.58 +  (see \S\ref{BasicOperationsOnTheories}).
    2.59 +
    2.60 +\item[\ttindexbold{qed} $name$]
    2.61 +  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
    2.62 +  result()} to get the theorem and then stores it like {\tt bind_thm}.
    2.63  \end{ttdescription}
    2.64  
    2.65  
    2.66 @@ -332,8 +345,10 @@
    2.67  \section{Executing batch proofs}
    2.68  \index{batch execution}
    2.69  \begin{ttbox}
    2.70 -prove_goal  :  theory->          string->(thm list->tactic list)->thm
    2.71 -prove_goalw :  theory->thm list->string->(thm list->tactic list)->thm
    2.72 +prove_goal :         theory->          string->(thm list->tactic list)->thm
    2.73 +qed_goal   : string->theory->          string->(thm list->tactic list)->unit
    2.74 +prove_goalw:         theory->thm list->string->(thm list->tactic list)->thm
    2.75 +qed_goalw  : string->theory->thm list->string->(thm list->tactic list)->unit
    2.76  prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
    2.77  \end{ttbox}
    2.78  These batch functions create an initial proof state, then apply a tactic to
    2.79 @@ -366,11 +381,19 @@
    2.80  executes a proof of the {\it formula\/} in the given {\it theory}, using
    2.81  the given tactic function.
    2.82  
    2.83 +\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
    2.84 +acts like {\tt prove_goal} but also stores the resulting theorem in
    2.85 +Isabelle's theorem database and in the ML variable $name$ (see
    2.86 +\S\ref{ExtractingAndStoringTheProvedTheorem}).
    2.87 +
    2.88  \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
    2.89        {\it tacsf};]\index{meta-rewriting}
    2.90  is like {\tt prove_goal} but also applies the list of {\it defs\/} as
    2.91  meta-rewrite rules to the first subgoal and the premises.
    2.92  
    2.93 +\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
    2.94 +is analogous to {\tt qed_goal}.
    2.95 +
    2.96  \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
    2.97        {\it tacsf};] 
    2.98  is a version of {\tt prove_goalw} for programming applications.  The main

     3.1 --- a/doc-src/Ref/theories.tex	Wed Jan 18 11:36:04 1995 +0100
     3.2 +++ b/doc-src/Ref/theories.tex	Thu Jan 19 16:05:21 1995 +0100
     3.3 @@ -308,7 +308,7 @@
     3.4  
     3.5  
     3.6  
     3.7 -\section{Basic operations on theories}
     3.8 +\section{Basic operations on theories}\label{BasicOperationsOnTheories}
     3.9  \subsection{Extracting an axiom or theorem from a theory}
    3.10  \index{theories!axioms of}\index{axioms!extracting}
    3.11  \index{theories!theorems of}\index{theorems!extracting}
    3.12 @@ -319,12 +319,14 @@
    3.13  \end{ttbox}
    3.14  \begin{ttdescription}
    3.15  \item[\ttindexbold{get_axiom} $thy$ $name$]
    3.16 -returns an axiom with the given $name$ from $thy$, raising exception
    3.17 -\xdx{THEORY} if none exists.  Merging theories can cause several axioms
    3.18 -to have the same name; {\tt get_axiom} returns an arbitrary one.
    3.19 +  returns an axiom with the given $name$ from $thy$, raising exception
    3.20 +  \xdx{THEORY} if none exists.  Merging theories can cause several axioms
    3.21 +  to have the same name; {\tt get_axiom} returns an arbitrary one.
    3.22  
    3.23  \item[\ttindexbold{get_thm} $thy$ $name$]
    3.24 -  is analogous to {\tt get_axiom}, but looks for a stored theorem.
    3.25 +  is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
    3.26 +  {\tt get_axiom} it searches all parents of a theory if the theorem
    3.27 +  is not associated with $thy$.
    3.28  
    3.29  \item[\ttindexbold{assume_ax} $thy$ $formula$]
    3.30    reads the {\it formula} using the syntax of $thy$, following the same
    3.31 @@ -427,7 +429,7 @@
    3.32  returns the additional axioms of the most recent extend node of~$thy$.
    3.33  
    3.34  \item[\ttindexbold{thms_of} $thy$]
    3.35 -similar to {\tt axioms_of}, but returns the stored theorems.
    3.36 +returns all theorems that are associated with $thy$.
    3.37  
    3.38  \item[\ttindexbold{parents_of} $thy$]
    3.39  returns the direct ancestors of~$thy$.

     4.1 --- a/doc-src/Ref/thm.tex	Wed Jan 18 11:36:04 1995 +0100
     4.2 +++ b/doc-src/Ref/thm.tex	Thu Jan 19 16:05:21 1995 +0100
     4.3 @@ -166,7 +166,7 @@
     4.4  \end{ttdescription}
     4.5  
     4.6  
     4.7 -\subsection{Miscellaneous forward rules}
     4.8 +\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
     4.9  \index{theorems!standardizing}
    4.10  \begin{ttbox} 
    4.11  standard         :           thm -> thm
    4.12 @@ -209,6 +209,7 @@
    4.13  nprems_of     : thm -> int
    4.14  tpairs_of     : thm -> (term*term)list
    4.15  stamps_of_thy : thm -> string ref list
    4.16 +theory_of_thm : thm -> theory
    4.17  dest_state    : thm*int -> (term*term)list*term list*term*term
    4.18  rep_thm       : thm -> \{prop:term, hyps:term list, 
    4.19                          maxidx:int, sign:Sign.sg\}
    4.20 @@ -230,6 +231,9 @@
    4.21  \item[\ttindexbold{stamps_of_thm} $thm$] 
    4.22  returns the \rmindex{stamps} of the signature associated with~$thm$.
    4.23  
    4.24 +\item[\ttindexbold{theory_of_thm} $thm$]
    4.25 +returns the theory associated with $thm$.
    4.26 +
    4.27  \item[\ttindexbold{dest_state} $(thm,i)$] 
    4.28  decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
    4.29  list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem