1.1 --- a/doc-src/IsarRef/Makefile Fri Jul 30 14:59:32 1999 +0200
1.2 +++ b/doc-src/IsarRef/Makefile Fri Jul 30 15:40:54 1999 +0200
1.3 @@ -14,7 +14,7 @@
1.4 NAME = isar-ref
1.5
1.6 FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
1.7 - clasimp.tex hol.tex ../isar.sty \
1.8 + generic.tex hol.tex ../isar.sty \
1.9 ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
1.10
1.11 dvi: $(NAME).dvi
2.1 --- a/doc-src/IsarRef/basics.tex Fri Jul 30 14:59:32 1999 +0200
2.2 +++ b/doc-src/IsarRef/basics.tex Fri Jul 30 15:40:54 1999 +0200
2.3 @@ -1,11 +1,13 @@
2.4
2.5 -\chapter{Basic concepts}
2.6 +\chapter{Basic Concepts}
2.7
2.8 \section{Isabelle/Isar Theories}
2.9
2.10 \section{The Isar proof language}
2.11
2.12 -\subsection{Proof methods}
2.13 +\subsection{Proof commands}
2.14 +
2.15 +\subsection{Methods}
2.16
2.17 \subsection{Attributes}
2.18
3.1 --- a/doc-src/IsarRef/clasimp.tex Fri Jul 30 14:59:32 1999 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,7 +0,0 @@
3.4 -
3.5 -\chapter{The Simplifier and Classical Reasoner}
3.6 -
3.7 -%%% Local Variables:
3.8 -%%% mode: latex
3.9 -%%% TeX-master: "isar-ref"
3.10 -%%% End:
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/IsarRef/generic.tex Fri Jul 30 15:40:54 1999 +0200
4.3 @@ -0,0 +1,60 @@
4.4 +
4.5 +\chapter{Generic Tools and Packages}
4.6 +
4.7 +\section{Axiomatic Type Classes}\label{sec:axclass}
4.8 +
4.9 +\indexisarcmd{axclass}\indexisarcmd{instance}
4.10 +\begin{matharray}{rcl}
4.11 + \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
4.12 + \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
4.13 +\end{matharray}
4.14 +
4.15 +Axiomatic type classes are provided by Isabelle/Pure as a purely
4.16 +\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus
4.17 +any object logic may make use of this light-weight mechanism for abstract
4.18 +theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a
4.19 +tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
4.20 +the standard Isabelle documentation.
4.21 +
4.22 +\begin{rail}
4.23 + 'axclass' classdecl (axmdecl prop comment? +)
4.24 + ;
4.25 + 'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
4.26 + ;
4.27 +\end{rail}
4.28 +
4.29 +\begin{description}
4.30 +\item [$\isarkeyword{axclass}~$] FIXME
4.31 +\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
4.32 + c@2$] setup up a goal stating the class relation or type arity. The proof
4.33 + would usually proceed by the $expand_classes$ method, and then establish the
4.34 + characteristic theorems of the type classes involved. After the final
4.35 + $\QED{}$, the theory will be augmented by a type signature declaration
4.36 + corresponding to the resulting theorem.
4.37 +\end{description}
4.38 +
4.39 +
4.40 +
4.41 +\section{The Simplifier}
4.42 +
4.43 +\section{The Classical Reasoner}
4.44 +
4.45 +
4.46 +%\indexisarcmd{}
4.47 +%\begin{matharray}{rcl}
4.48 +% \isarcmd{} & : & \isartrans{}{} \\
4.49 +%\end{matharray}
4.50 +
4.51 +%\begin{rail}
4.52 +
4.53 +%\end{rail}
4.54 +
4.55 +%\begin{description}
4.56 +%\item [$ $]
4.57 +%\end{description}
4.58 +
4.59 +
4.60 +%%% Local Variables:
4.61 +%%% mode: latex
4.62 +%%% TeX-master: "isar-ref"
4.63 +%%% End:
5.1 --- a/doc-src/IsarRef/hol.tex Fri Jul 30 14:59:32 1999 +0200
5.2 +++ b/doc-src/IsarRef/hol.tex Fri Jul 30 15:40:54 1999 +0200
5.3 @@ -1,5 +1,16 @@
5.4
5.5 -\chapter{Isabelle/HOL specific elements}
5.6 +\chapter{Isabelle/HOL specific tools and packages}
5.7 +
5.8 +\section{Primitive types}
5.9 +
5.10 +\section{Records}
5.11 +
5.12 +\section{Datatypes}
5.13 +
5.14 +\section{Recursive functions}
5.15 +
5.16 +\section{(Co)Inductive sets}
5.17 +
5.18
5.19 %%% Local Variables:
5.20 %%% mode: latex
6.1 --- a/doc-src/IsarRef/isar-ref.tex Fri Jul 30 14:59:32 1999 +0200
6.2 +++ b/doc-src/IsarRef/isar-ref.tex Fri Jul 30 15:40:54 1999 +0200
6.3 @@ -56,7 +56,7 @@
6.4 \include{basics}
6.5 \include{syntax}
6.6 \include{pure}
6.7 -\include{clasimp}
6.8 +\include{generic}
6.9 \include{hol}
6.10
6.11 \begingroup
7.1 --- a/doc-src/IsarRef/pure.tex Fri Jul 30 14:59:32 1999 +0200
7.2 +++ b/doc-src/IsarRef/pure.tex Fri Jul 30 15:40:54 1999 +0200
7.3 @@ -105,7 +105,7 @@
7.4 \end{description}
7.5
7.6
7.7 -\subsection{Type classes and sorts}
7.8 +\subsection{Type classes and sorts}\label{sec:classes}
7.9
7.10 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
7.11 \begin{matharray}{rcl}
7.12 @@ -115,7 +115,7 @@
7.13 \end{matharray}
7.14
7.15 \begin{rail}
7.16 - 'classes' (name ('<' (nameref ',' +))? comment? +)
7.17 + 'classes' (classdecl +)
7.18 ;
7.19 'classrel' nameref '<' nameref comment?
7.20 ;
7.21 @@ -253,7 +253,7 @@
7.22 \end{matharray}
7.23
7.24 \begin{rail}
7.25 - 'axioms' (name attributes? ':' prop comment? +)
7.26 + 'axioms' (axmdecl prop comment? +)
7.27 ;
7.28 ('theorems' | 'lemmas') thmdef? thmrefs
7.29 ;
8.1 --- a/doc-src/IsarRef/syntax.tex Fri Jul 30 14:59:32 1999 +0200
8.2 +++ b/doc-src/IsarRef/syntax.tex Fri Jul 30 15:40:54 1999 +0200
8.3 @@ -74,6 +74,7 @@
8.4 ever refer to sorts or arities explicitly.
8.5
8.6 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
8.7 +\indexouternonterm{classdecl}
8.8 \begin{rail}
8.9 sort : nameref | lbrace (nameref * ',') rbrace
8.10 ;
8.11 @@ -81,6 +82,7 @@
8.12 ;
8.13 simplearity : ( () | '(' (sort + ',') ')' ) nameref
8.14 ;
8.15 + classdecl: name ('<' (nameref ',' +))? comment?
8.16 \end{rail}
8.17
8.18
8.19 @@ -181,10 +183,13 @@
8.20 as proof method arguments). Any of these may include lists of attributes,
8.21 which are applied to the preceding theorem or list of theorems.
8.22
8.23 -\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
8.24 +\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
8.25 +\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
8.26 \begin{rail}
8.27 thmname : name attributes | name | attributes
8.28 ;
8.29 + axmdecl : name attributes? ':'
8.30 + ;
8.31 thmdecl : thmname ':'
8.32 ;
8.33 thmdef : thmname '='