# HG changeset patch
# User wenzelm
# Date 909138683 -7200
# Node ID 6b8bb85c384808ae55185d1291aae8dc93869e44
# Parent  bebd10cb7a8d10b989f6ebbe275a2981a8518541
started to add records;

diff -r bebd10cb7a8d -r 6b8bb85c3848 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Oct 23 11:03:35 1998 +0200
+++ b/doc-src/Logics/HOL.tex	Fri Oct 23 12:31:23 1998 +0200
@@ -1539,6 +1539,42 @@
 class of all \HOL\ types.
 \end{warn}
 
+
+\section{Record types}
+
+At a first approximation, records are just a minor generalization of tuples,
+where components may be addressed by labels instead of just position.  The
+version of records offered by Isabelle/HOL is slightly more advanced, though,
+supporting \emph{extensible record schemes}.  This admits polymorphic
+operations wrt.\ record extensions, yielding ``object-oriented'' effects like
+(single) inheritance.  See also \cite{Naraschewski-Wenzel:1998:TPHOL} for more
+details on object-oriented verification and record subtyping in HOL.
+
+\subsection{Defining records}
+
+\begin{figure}[htbp]
+\begin{rail}
+record  : 'record' typevarlist name '=' parent (field +);
+parent  : ( () | type '+');
+field   : name '::' type;
+\end{rail}
+\caption{Syntax of record type definitions}
+\label{fig:HOL:record}
+\end{figure}
+
+Records have to be defined explicitely, fixing their field names and types,
+and (optional) parent record scheme.  The theory syntax for record type
+definitions is shown in Fig.~\ref{fig:HOL:record}.  For the definition of
+`typevarlist' and `type' see \iflabelundefined{chap:classical}
+{the appendix of the {\em Reference Manual\/}}%
+{Appendix~\ref{app:TheorySyntax}}.
+
+
+\subsection{Record operations and syntax}
+
+\subsection{Proof tools}
+
+
 \section{Datatype declarations}
 \label{sec:HOL:datatype}
 \index{*datatype|(}
@@ -2538,3 +2574,8 @@
 \ttindex{set_current_thy}~{\tt"Set"}.  Otherwise the default claset may not
 contain the rules for set theory.
 \index{higher-order logic|)}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "logics"
+%%% End: 
diff -r bebd10cb7a8d -r 6b8bb85c3848 doc-src/Logics/logics.rao
--- a/doc-src/Logics/logics.rao	Fri Oct 23 11:03:35 1998 +0200
+++ b/doc-src/Logics/logics.rao	Fri Oct 23 12:31:23 1998 +0200
@@ -36,8 +36,34 @@
 \rail@endbar
 \rail@end
 }
-\rail@i {2}{ typedecl : typevarlist id '=' (cons + '|') ; cons : name (typ *) ( () | mixfix ) ; typ : id | tid | ('(' typevarlist id ')') ; }
+\rail@i {2}{ record : 'record' typevarlist name '=' parent (field +); parent : ( () | type '+'); field : name '::' type; }
 \rail@o {2}{
+\rail@begin{2}{record}
+\rail@term{record}[]
+\rail@nont{typevarlist}[]
+\rail@nont{name}[]
+\rail@term{=}[]
+\rail@nont{parent}[]
+\rail@plus
+\rail@nont{field}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{parent}
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{type}[]
+\rail@term{+}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{field}
+\rail@nont{name}[]
+\rail@term{::}[]
+\rail@nont{type}[]
+\rail@end
+}
+\rail@i {3}{ typedecl : typevarlist id '=' (cons + '|') ; cons : name (typ *) ( () | mixfix ) ; typ : id | tid | ('(' typevarlist id ')') ; }
+\rail@o {3}{
 \rail@begin{2}{typedecl}
 \rail@nont{typevarlist}[]
 \rail@nont{id}[]