1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Jul 30 15:40:54 1999 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +
     1.5 +\chapter{Generic Tools and Packages}
     1.6 +
     1.7 +\section{Axiomatic Type Classes}\label{sec:axclass}
     1.8 +
     1.9 +\indexisarcmd{axclass}\indexisarcmd{instance}
    1.10 +\begin{matharray}{rcl}
    1.11 +  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
    1.12 +  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    1.13 +\end{matharray}
    1.14 +
    1.15 +Axiomatic type classes are provided by Isabelle/Pure as a purely
    1.16 +\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
    1.17 +any object logic may make use of this light-weight mechanism for abstract
    1.18 +theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
    1.19 +tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
    1.20 +the standard Isabelle documentation.
    1.21 +
    1.22 +\begin{rail}
    1.23 +  'axclass' classdecl (axmdecl prop comment? +)
    1.24 +  ;
    1.25 +  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
    1.26 +  ;
    1.27 +\end{rail}
    1.28 +
    1.29 +\begin{description}
    1.30 +\item [$\isarkeyword{axclass}~$] FIXME
    1.31 +\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
    1.32 +  c@2$] setup up a goal stating the class relation or type arity.  The proof
    1.33 +  would usually proceed by the $expand_classes$ method, and then establish the
    1.34 +  characteristic theorems of the type classes involved.  After the final
    1.35 +  $\QED{}$, the theory will be augmented by a type signature declaration
    1.36 +  corresponding to the resulting theorem.
    1.37 +\end{description}
    1.38 +
    1.39 +
    1.40 +
    1.41 +\section{The Simplifier}
    1.42 +
    1.43 +\section{The Classical Reasoner}
    1.44 +
    1.45 +
    1.46 +%\indexisarcmd{}
    1.47 +%\begin{matharray}{rcl}
    1.48 +%  \isarcmd{} & : & \isartrans{}{} \\
    1.49 +%\end{matharray}
    1.50 +
    1.51 +%\begin{rail}
    1.52 +  
    1.53 +%\end{rail}
    1.54 +
    1.55 +%\begin{description}
    1.56 +%\item [$ $]
    1.57 +%\end{description}
    1.58 +
    1.59 +
    1.60 +%%% Local Variables: 
    1.61 +%%% mode: latex
    1.62 +%%% TeX-master: "isar-ref"
    1.63 +%%% End: