--- a/doc-src/HOL/HOL.tex Mon May 02 21:33:21 2011 +0200
+++ b/doc-src/HOL/HOL.tex Mon May 02 21:41:39 2011 +0200
@@ -1620,34 +1620,9 @@
then the type definition creates a type constructor
$(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
-\begin{figure}[htbp]
-\begin{rail}
-typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
-
-type : typevarlist name ( () | '(' infix ')' );
-set : string;
-witness : () | '(' id ')';
-\end{rail}
-\caption{Syntax of type definitions}
-\label{fig:HOL:typedef}
-\end{figure}
-
-The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
-the definition of `typevarlist' and `infix' see
-\iflabelundefined{chap:classical}
-{the appendix of the {\em Reference Manual\/}}%
-{Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
-following meaning:
-\begin{description}
-\item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
- optional infix annotation.
-\item[\it name:] an alphanumeric name $T$ for the type constructor
- $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
-\item[\it set:] the representing subset $A$.
-\item[\it witness:] name of a theorem of the form $a:A$ proving
- non-emptiness. It can be omitted in case Isabelle manages to prove
- non-emptiness automatically.
-\end{description}
+The syntax for type definitions is given in the Isabelle/Isar
+reference manual.
+
If all context conditions are met (no duplicate type variables in
`typevarlist', no extra type variables in `set', and no free term variables
in `set'), the following components are added to the theory:
@@ -1986,28 +1961,11 @@
\subsection{Defining datatypes}
-The theory syntax for datatype definitions is shown in
-Fig.~\ref{datatype-grammar}. In order to be well-formed, a datatype
-definition has to obey the rules stated in the previous section. As a result
-the theory is extended with the new types, the constructors, and the theorems
-listed in the previous section.
-
-\begin{figure}
-\begin{rail}
-datatype : 'datatype' typedecls;
-
-typedecls: ( newtype '=' (cons + '|') ) + 'and'
- ;
-newtype : typevarlist id ( () | '(' infix ')' )
- ;
-cons : name (argtype *) ( () | ( '(' mixfix ')' ) )
- ;
-argtype : id | tid | ('(' typevarlist id ')')
- ;
-\end{rail}
-\caption{Syntax of datatype declarations}
-\label{datatype-grammar}
-\end{figure}
+The theory syntax for datatype definitions is given in the
+Isabelle/Isar reference manual. In order to be well-formed, a
+datatype definition has to obey the rules stated in the previous
+section. As a result the theory is extended with the new types, the
+constructors, and the theorems listed in the previous section.
Most of the theorems about datatypes become part of the default simpset and
you never need to see them again because the simplifier applies them
--- a/doc-src/HOL/Makefile Mon May 02 21:33:21 2011 +0200
+++ b/doc-src/HOL/Makefile Mon May 02 21:41:39 2011 +0200
@@ -1,6 +1,3 @@
-#
-# $Id$
-#
## targets
@@ -13,10 +10,7 @@
NAME = logics-HOL
FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \
- ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
-
-rail:
- $(RAIL) $(NAME)
+ ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
dvi: $(NAME).dvi
--- a/doc-src/HOL/logics-HOL.rai Mon May 02 21:33:21 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-\rail@i{1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par
-type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
-\rail@i{2}{ datatype : 'datatype' typedecls; \par
-typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
--- a/doc-src/HOL/logics-HOL.rao Mon May 02 21:33:21 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,210 +0,0 @@
-% This file was generated by 'rail' from 'logics-HOL.rai'
-\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par
-type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
-\rail@o {1}{
-\rail@begin{2}{typedef}
-\rail@term{typedef}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{(}[]
-\rail@nont{name}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@nont{type}[]
-\rail@term{=}[]
-\rail@nont{set}[]
-\rail@nont{witness}[]
-\rail@end
-\rail@begin{2}{type}
-\rail@nont{typevarlist}[]
-\rail@nont{name}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{(}[]
-\rail@nont{infix}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{set}
-\rail@nont{string}[]
-\rail@end
-\rail@begin{2}{witness}
-\rail@bar
-\rail@nextbar{1}
-\rail@term{(}[]
-\rail@nont{id}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@end
-}
-\rail@i {2}{ datatype : 'datatype' typedecls; \par
-typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
-\rail@o {2}{
-\rail@begin{1}{datatype}
-\rail@term{datatype}[]
-\rail@nont{typedecls}[]
-\rail@end
-\rail@begin{3}{typedecls}
-\rail@plus
-\rail@nont{newtype}[]
-\rail@term{=}[]
-\rail@plus
-\rail@nont{cons}[]
-\rail@nextplus{1}
-\rail@cterm{|}[]
-\rail@endplus
-\rail@nextplus{2}
-\rail@cterm{and}[]
-\rail@endplus
-\rail@end
-\rail@begin{2}{newtype}
-\rail@nont{typevarlist}[]
-\rail@nont{id}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{(}[]
-\rail@nont{infix}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{cons}
-\rail@nont{name}[]
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{argtype}[]
-\rail@endplus
-\rail@bar
-\rail@nextbar{1}
-\rail@term{(}[]
-\rail@nont{mixfix}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@end
-\rail@begin{3}{argtype}
-\rail@bar
-\rail@nont{id}[]
-\rail@nextbar{1}
-\rail@nont{tid}[]
-\rail@nextbar{2}
-\rail@term{(}[]
-\rail@nont{typevarlist}[]
-\rail@nont{id}[]
-\rail@term{)}[]
-\rail@endbar
-\rail@end
-}
-\rail@t {verblbrace}
-\rail@t {verbrbrace}
-\rail@i {3}{ codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); \par
-modespec : '(' ( name * ) ')'; }
-\rail@o {3}{
-\rail@begin{11}{codegen}
-\rail@bar
-\rail@term{code_module}[]
-\rail@nextbar{1}
-\rail@term{code_library}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{modespec}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{name}[]
-\rail@endbar
-\rail@cr{3}
-\rail@bar
-\rail@nextbar{4}
-\rail@term{file}[]
-\rail@nont{name}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{4}
-\rail@term{imports}[]
-\rail@plus
-\rail@nont{name}[]
-\rail@nextplus{5}
-\rail@endplus
-\rail@endbar
-\rail@cr{7}
-\rail@term{contains}[]
-\rail@bar
-\rail@plus
-\rail@nont{name}[]
-\rail@term{=}[]
-\rail@nont{term}[]
-\rail@nextplus{8}
-\rail@endplus
-\rail@nextbar{9}
-\rail@plus
-\rail@nont{term}[]
-\rail@nextplus{10}
-\rail@endplus
-\rail@endbar
-\rail@end
-\rail@begin{2}{modespec}
-\rail@term{(}[]
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{name}[]
-\rail@endplus
-\rail@term{)}[]
-\rail@end
-}
-\rail@i {4}{ constscode : 'consts_code' (codespec +); \par
-codespec : const template attachment ?; \par
-typescode : 'types_code' (tycodespec +); \par
-tycodespec : name template attachment ?; \par
-const : term; \par
-template: '(' string ')'; \par
-attachment: 'attach' modespec ? verblbrace text verbrbrace; }
-\rail@o {4}{
-\rail@begin{2}{constscode}
-\rail@term{consts_code}[]
-\rail@plus
-\rail@nont{codespec}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{2}{codespec}
-\rail@nont{const}[]
-\rail@nont{template}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{attachment}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{typescode}
-\rail@term{types_code}[]
-\rail@plus
-\rail@nont{tycodespec}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{2}{tycodespec}
-\rail@nont{name}[]
-\rail@nont{template}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{attachment}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{const}
-\rail@nont{term}[]
-\rail@end
-\rail@begin{1}{template}
-\rail@term{(}[]
-\rail@nont{string}[]
-\rail@term{)}[]
-\rail@end
-\rail@begin{2}{attachment}
-\rail@term{attach}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{modespec}[]
-\rail@endbar
-\rail@token{verblbrace}[]
-\rail@nont{text}[]
-\rail@token{verbrbrace}[]
-\rail@end
-}
--- a/doc-src/HOL/logics-HOL.tex Mon May 02 21:33:21 2011 +0200
+++ b/doc-src/HOL/logics-HOL.tex Mon May 02 21:41:39 2011 +0200
@@ -1,7 +1,7 @@
%% $Id$
\documentclass[12pt,a4paper]{report}
\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,latexsym,../pdfsetup}
+\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}