--- 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
--- 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}
--- 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:
--- /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:
--- 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
--- 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
--- 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
;
--- 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 '='