--- a/doc-src/IsarRef/generic.tex Mon Aug 23 09:36:05 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Mon Aug 23 11:43:21 1999 +0200
@@ -154,6 +154,7 @@
\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
@@ -178,8 +179,12 @@
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.
+\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}
@@ -194,13 +199,15 @@
\end{matharray}
\begin{rail}
- 'simp' (simpmod+)?
+ 'simp' (simpmod * )
;
simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
;
\end{rail}
+FIXME
+
\subsection{Forward simplification}