\chapter{Generic Tools and Packages}\label{ch:gen-tools}
\section{Basic proof methods and attributes}\label{sec:pure-meth}
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
\indexisarmeth{rule}\indexisarmeth{erule}
\begin{matharray}{rcl}
fail & : & \isarmeth \\
succeed & : & \isarmeth \\
- & : & \isarmeth \\
assumption & : & \isarmeth \\
finish & : & \isarmeth \\
fold & : & \isarmeth \\
unfold & : & \isarmeth \\
rule & : & \isarmeth \\
erule^* & : & \isarmeth \\
\end{matharray}
\begin{rail}
('fold' | 'unfold' | 'rule' | 'erule') thmrefs
;
\end{rail}
\begin{descr}
\item [$ $]
\end{descr}
FIXME
%FIXME sort
%FIXME thmref (single)
%FIXME var vs. term
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
\begin{matharray}{rcl}
tag & : & \isaratt \\
untag & : & \isaratt \\
COMP & : & \isaratt \\
RS & : & \isaratt \\
OF & : & \isaratt \\
where & : & \isaratt \\
of & : & \isaratt \\
standard & : & \isaratt \\
elimify & : & \isaratt \\
transfer & : & \isaratt \\
export & : & \isaratt \\
\end{matharray}
\begin{rail}
('tag' | 'untag') (nameref+)
;
('COMP' | 'RS') nat? thmref
;
'OF' thmrefs
;
'where' (term '=' term * 'and')
;
'of' (inst * ) ('concl:' (inst * ))?
;
inst: underscore | term
;
\end{rail}
\begin{descr}
\item [$ $]
\end{descr}
FIXME
\section{Axiomatic Type Classes}\label{sec:axclass}
\indexisarcmd{axclass}\indexisarcmd{instance}
\begin{matharray}{rcl}
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}
Axiomatic type classes are provided by Isabelle/Pure as a purely
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus
any object logic may make use of this light-weight mechanism for abstract
theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
the standard Isabelle documentation.
\begin{rail}
'axclass' classdecl (axmdecl prop comment? +)
;
'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
;
\end{rail}
\begin{descr}
\item [$\isarkeyword{axclass}~$] FIXME
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
c@2$] setup up a goal stating the class relation or type arity. The proof
would usually proceed by the $expand_classes$ method, and then establish the
characteristic theorems of the type classes involved. After finishing the
proof the theory will be augmented by a type signature declaration
corresponding to the resulting theorem.
\end{descr}
\section{The Simplifier}
\section{The Classical Reasoner}
%\indexisarcmd{}
%\begin{matharray}{rcl}
% \isarcmd{} & : & \isartrans{}{} \\
%\end{matharray}
%\begin{rail}
%\end{rail}
%\begin{descr}
%\item [$ $]
%\end{descr}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: