doc-src/IsarRef/generic.tex

even more stuff;

\chapter{Generic Tools and Packages}

\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{description}
\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{description}



\section{The Simplifier}

\section{The Classical Reasoner}


%\indexisarcmd{}
%\begin{matharray}{rcl}
%  \isarcmd{} & : & \isartrans{}{} \\
%\end{matharray}

%\begin{rail}
  
%\end{rail}

%\begin{description}
%\item [$ $]
%\end{description}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: