%
\begin{isabellebody}%
\def\isabellecontext{proof}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Structured reasoning%
}
\isamarkuptrue%
%
\isamarkupsection{Proof context%
}
\isamarkuptrue%
%
\isamarkupsubsection{Local variables%
}
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
\indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> thm list * Proof.context| \\
\indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
\indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\
\indexml{Variable.monomorphic}\verb|Variable.monomorphic: Proof.context -> term list -> term list| \\
\indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
\end{mldecls}
\begin{description}
\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| 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.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| introduces fixed type variables for
the schematic of the given facts.
\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}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof state%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME
\glossary{Proof state}{The whole configuration of a structured proof,
consisting of a \seeglossary{proof context} and an optional
\seeglossary{structured goal}. Internally, an Isar proof state is
organized as a stack to accomodate block structure of proof texts.
For historical reasons, a low-level \seeglossary{tactical goal} is
occasionally called ``proof state'' as well.}
\glossary{Structured goal}{FIXME}
\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Methods%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Attributes%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: