doc-src/IsarRef/generic.tex

 
 \indexisarcmd{axclass}\indexisarcmd{instance}
 \begin{matharray}{rcl}
   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
+  expand_classes & : & \isarmeth \\
 \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

   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}
-
+\item [Method $expand_classes$] iteratively expands the class introduction
+  rules
+\end{descr}
+
+See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
+axiomatic type classes, including instantiation proofs.
 
 
 \section{The Simplifier}
 
 \subsection{Simplification methods}

   asm_simp & : & \isarmeth \\
   simp & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
-  'simp' (simpmod+)?
+  'simp' (simpmod * )
   ;
 
   simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
   ;
 \end{rail}
+
+FIXME
 
 
 \subsection{Forward simplification}
 
 \indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}