# HG changeset patch
# User wenzelm
# Date 933342054 -7200
# Node ID 8eabfd7e6b9b6d099801a62206c817ccf6bf9cc3
# Parent  320b412e5800687b539f8d08a5b660c2a6477757
more;

diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/Makefile
--- a/doc-src/IsarRef/Makefile	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/Makefile	Fri Jul 30 15:40:54 1999 +0200
@@ -14,7 +14,7 @@
 NAME = isar-ref
 
 FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
-	clasimp.tex hol.tex ../isar.sty \
+	generic.tex hol.tex ../isar.sty \
 	../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
 
 dvi: $(NAME).dvi
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/basics.tex
--- a/doc-src/IsarRef/basics.tex	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/basics.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -1,11 +1,13 @@
 
-\chapter{Basic concepts}
+\chapter{Basic Concepts}
 
 \section{Isabelle/Isar Theories}
 
 \section{The Isar proof language}
 
-\subsection{Proof methods}
+\subsection{Proof commands}
+
+\subsection{Methods}
 
 \subsection{Attributes}
 
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/clasimp.tex
--- a/doc-src/IsarRef/clasimp.tex	Fri Jul 30 14:59:32 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-
-\chapter{The Simplifier and Classical Reasoner}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "isar-ref"
-%%% End: 
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/generic.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/generic.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -0,0 +1,60 @@
+
+\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 the final
+  $\QED{}$, 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: 
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/hol.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -1,5 +1,16 @@
 
-\chapter{Isabelle/HOL specific elements}
+\chapter{Isabelle/HOL specific tools and packages}
+
+\section{Primitive types}
+
+\section{Records}
+
+\section{Datatypes}
+
+\section{Recursive functions}
+
+\section{(Co)Inductive sets}
+
 
 %%% Local Variables: 
 %%% mode: latex
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -56,7 +56,7 @@
 \include{basics}
 \include{syntax}
 \include{pure}
-\include{clasimp}
+\include{generic}
 \include{hol}
 
 \begingroup
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -105,7 +105,7 @@
 \end{description}
 
 
-\subsection{Type classes and sorts}
+\subsection{Type classes and sorts}\label{sec:classes}
 
 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
 \begin{matharray}{rcl}
@@ -115,7 +115,7 @@
 \end{matharray}
 
 \begin{rail}
-  'classes' (name ('<' (nameref ',' +))? comment? +)
+  'classes' (classdecl +)
   ;
   'classrel' nameref '<' nameref comment?
   ;
@@ -253,7 +253,7 @@
 \end{matharray}
 
 \begin{rail}
-  'axioms' (name attributes? ':' prop comment? +)
+  'axioms' (axmdecl prop comment? +)
   ;
   ('theorems' | 'lemmas') thmdef? thmrefs
   ;
diff -r 320b412e5800 -r 8eabfd7e6b9b doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -74,6 +74,7 @@
 ever refer to sorts or arities explicitly.
 
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
+\indexouternonterm{classdecl}
 \begin{rail}
   sort : nameref | lbrace (nameref * ',') rbrace
   ;
@@ -81,6 +82,7 @@
   ;
   simplearity : ( () | '(' (sort + ',') ')' ) nameref
   ;
+  classdecl: name ('<' (nameref ',' +))? comment?
 \end{rail}
 
 
@@ -181,10 +183,13 @@
 as proof method arguments).  Any of these may include lists of attributes,
 which are applied to the preceding theorem or list of theorems.
 
-\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
+\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
+\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
 \begin{rail}
   thmname : name attributes | name | attributes
   ;
+  axmdecl : name attributes? ':'
+  ;
   thmdecl : thmname ':'
   ;
   thmdef : thmname '='