--- a/doc-src/IsarImplementation/Thy/document/proof.tex Sat Jul 08 12:54:28 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Sat Jul 08 12:54:29 2006 +0200
@@ -49,17 +49,30 @@
\begin{description}
- \item \verb|Variable.declare_term| FIXME
+ \item \verb|Variable.declare_term| declares a term as belonging to
+ the current context. This fixes free type variables, but not term
+ variables; constraints for type and term variables are declared
+ uniformly.
- \item \verb|Variable.import| FIXME
-
- \item \verb|Variable.export| FIXME
+ \item \verb|Variable.import| introduces new fixes for schematic type
+ and term variables occurring in given facts. The effect may be
+ reversed (up to renaming) via \verb|Variable.export|.
- \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|.
+ \item \verb|Variable.export| generalizes fixed type and term
+ variables according to the difference of the two contexts. Note
+ that type variables occurring in term variables are still fixed,
+ even though they got introduced later (e.g.\ by type-inference).
+
+ \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all
+ variables being fixed in the current context.
- \item \verb|Variable.monomorphic| FIXME
+ \item \verb|Variable.monomorphic| introduces fixed type variables for
+ the schematic of the given facts.
- \item \verb|Variable.polymorphic| FIXME
+ \item \verb|Variable.polymorphic| generalizes type variables as far
+ as possible, even those occurring in fixed term variables. This
+ operation essentially reverses the default policy of type-inference
+ to introduce local polymorphism entities in fixed form.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 12:54:28 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Sat Jul 08 12:54:29 2006 +0200
@@ -195,15 +195,17 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{Goal.prove}\verb|Goal.prove: theory -> string list -> term list -> term ->|\isasep\isanewline%
+ \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
\verb| (thm list -> tactic) -> thm| \\
- \indexml{Goal.prove-multi}\verb|Goal.prove_multi: theory -> string list -> term list -> term list ->|\isasep\isanewline%
+ \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb| (thm list -> tactic) -> thm list| \\
+ \indexml{Goal.prove-global}\verb|Goal.prove_global: theory -> string list -> term list -> term ->|\isasep\isanewline%
+\verb| (thm list -> tactic) -> thm| \\
\end{mldecls}
\begin{description}
- \item \verb|Goal.prove|~\isa{thy\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
+ \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
and hypotheses \isa{As} and applies tactic \isa{tac} to
solve it. The latter may depend on the local assumptions being
presented as facts. The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
@@ -219,6 +221,8 @@
states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
subgoals before commencing the actual proof.
+ \item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%