# HG changeset patch
# User wenzelm
# Date 933352045 -7200
# Node ID a67dde8820c02eaff5be128a97e6e0fb1261c8f2
# Parent  2c02c8e212fa9c7d86b7c0d03ba9bf21ca56ab55
even more stuff;

diff -r 2c02c8e212fa -r a67dde8820c0 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Jul 30 18:27:25 1999 +0200
@@ -28,8 +28,8 @@
 \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
+  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{description}
 
diff -r 2c02c8e212fa -r a67dde8820c0 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/hol.tex	Fri Jul 30 18:27:25 1999 +0200
@@ -1,16 +1,143 @@
 
-\chapter{Isabelle/HOL specific tools and packages}
+\chapter{Isabelle/HOL Tools and Packages}
 
 \section{Primitive types}
 
-\section{Records}
+\indexisarcmd{typedecl}\indexisarcmd{typedef}
+\begin{matharray}{rcl}
+  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
+  \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
+\end{matharray}
+
+\begin{rail}
+  'typedecl' typespec infix? comment?
+  ;
+  'typedef' parname? typespec infix? \\ '=' term comment?
+  ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
+  $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
+  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
+  actual HOL type constructor.
+\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
+  non-emptiness of the set $A$.  After finishing the proof, the theory will be
+  augmented by a Gordon/HOL-style type definitions.  See \cite{isabelle-HOL}
+  for more information.  Note that user-level work usually does not directly
+  refer to the HOL $\isarkeyword{typedef}$ primitive, but uses more advanced
+  packages such as $\isarkeyword{record}$ (\S\ref{sec:record}) or
+  $\isarkeyword{datatype}$ (\S\ref{sec:datatype}).
+\end{description}
+
+
+\section{Records}\label{sec:record}
+
+%FIXME record_split method
+\indexisarcmd{record}
+\begin{matharray}{rcl}
+  \isarcmd{record} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+  'record' typespec '=' (type '+')? (field +)
+  ;
 
-\section{Datatypes}
+  field: name '::' type comment?
+  ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$]
+  defines extensible record type $(\vec\alpha)t$, derived from the optional
+  parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$.
+  See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only
+  simply-typed records.
+\end{description}
+
+
+\section{Datatypes}\label{sec:datatype}
+
+\indexisarcmd{datatype}\indexisarcmd{rep_datatype}
+\begin{matharray}{rcl}
+  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
+  \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{repdatatype}{rep\_datatype}
+\railterm{repdatatype}
+
+\begin{rail}
+  'datatype' (parname? typespec infix? \\ '=' (cons + '|') + 'and')
+  ;
+  repdatatype (name * ) \\ 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
+  ;
+
+  cons: name (type * ) mixfix? comment?
+  ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{datatype}$] FIXME
+\item [$\isarkeyword{rep_datatype}$] FIXME
+\end{description}
+
 
 \section{Recursive functions}
 
+\indexisarcmd{primrec}\indexisarcmd{recdef}
+\begin{matharray}{rcl}
+  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
+  \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
+%FIXME
+%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\begin{rail}
+  'primrec' parname? (thmdecl? prop comment? + )
+  ;
+  'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
+  ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{primrec}$] FIXME
+\item [$\isarkeyword{recdef}$] FIXME
+\end{description}
+
+
 \section{(Co)Inductive sets}
 
+\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive\_cases}
+\begin{matharray}{rcl}
+  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
+  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
+\end{matharray}
+
+\railalias{condefs}{con\_defs}
+\railalias{indcases}{inductive\_cases}
+\railterm{condefs,indcases}
+
+\begin{rail}
+  ('inductive' | 'coinductive') (term comment? +) \\
+    'intrs' attributes? (thmdecl? prop comment? +) \\
+    'monos' thmrefs comment? \\ condefs thmrefs comment?
+  ;
+  indcases thmdef? nameref ':' \\ (prop +) comment?
+  ;
+\end{rail}
+
+\begin{description}
+\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME
+\item [$\isarkeyword{inductive_cases}$] FIXME
+\end{description}
+
+
+\section{Proof by induction}
+
+%FIXME induct proof method
+
 
 %%% Local Variables: 
 %%% mode: latex
diff -r 2c02c8e212fa -r a67dde8820c0 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/pure.tex	Fri Jul 30 18:27:25 1999 +0200
@@ -136,7 +136,7 @@
 \end{description}
 
 
-\subsection{Types}
+\subsection{Types}\label{sec:types-pure}
 
 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
 \begin{matharray}{rcl}
@@ -327,9 +327,9 @@
 
 \subsection{ML translation functions}
 
-\indexisarcmd{parse_ast_translation}\indexisarcmd{parse_translation}
-\indexisarcmd{print_translation}\indexisarcmd{typed_print_translation}
-\indexisarcmd{print_ast_translation}\indexisarcmd{token_translation}
+\indexisarcmd{parse\_ast\_translation}\indexisarcmd{parse\_translation}
+\indexisarcmd{print\_translation}\indexisarcmd{typed\_print\_translation}
+\indexisarcmd{print\_ast\_translation}\indexisarcmd{token\_translation}
 \begin{matharray}{rcl}
   \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
   \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
@@ -367,7 +367,8 @@
 
 \subsection{Goal statements}
 
-\indexisarcmd{}
+\indexisarcmd{theorem}\indexisarcmd{lemma}
+\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
 \begin{matharray}{rcl}
   \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
   \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
@@ -495,15 +496,6 @@
   \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
 \end{matharray}
 
-\begin{rail}
-  llbrace
-  ;
-  rrbrace
-  ;
-  'next'
-  ;
-\end{rail}
-
 \begin{description}
 \item [$ $] FIXME
 \end{description}
@@ -533,7 +525,7 @@
 
 \subsection{Improper proof steps}
 
-\indexisarcmd{apply}\indexisarcmd{then_apply}\indexisarcmd{back}
+\indexisarcmd{apply}\indexisarcmd{then\_apply}\indexisarcmd{back}
 \begin{matharray}{rcl}
   \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
   \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
@@ -593,8 +585,8 @@
 
 \subsection{System operations}
 
-\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use_thy}\indexisarcmd{use_thy_only}
-\indexisarcmd{update_thy}\indexisarcmd{update_thy_only}
+\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use\_thy}\indexisarcmd{use\_thy\_only}
+\indexisarcmd{update\_thy}\indexisarcmd{update\_thy\_only}
 \begin{matharray}{rcl}
   \isarcmd{cd} & : & \isarkeep{\cdot} \\
   \isarcmd{pwd} & : & \isarkeep{\cdot} \\
diff -r 2c02c8e212fa -r a67dde8820c0 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Fri Jul 30 18:27:25 1999 +0200
@@ -35,10 +35,12 @@
 \verb|"let"|).  Already existing objects are usually referenced by
 \railqtoken{nameref}.
 
-\indexoutertoken{name}\indexoutertoken{nameref}
+\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
 \begin{rail}
   name : ident | symident | string
   ;
+  parname : '(' name ')'
+  ;
   nameref : name | longident
   ;
 \end{rail}