# HG changeset patch
# User wenzelm
# Date 1304365299 -7200
# Node ID 50f257ea2aba6b788be7d49c0a971396ebfd3de2
# Parent  8749742785b8cfe2519c8264a25756a24eb02a15
removed obsolete rail diagrams (which were about old-style theory syntax);

diff -r 8749742785b8 -r 50f257ea2aba doc-src/HOL/HOL.tex
--- 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
diff -r 8749742785b8 -r 50f257ea2aba doc-src/HOL/Makefile
--- 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
 
diff -r 8749742785b8 -r 50f257ea2aba doc-src/HOL/logics-HOL.rai
--- 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 ')') ; }
diff -r 8749742785b8 -r 50f257ea2aba doc-src/HOL/logics-HOL.rao
--- 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
-}
diff -r 8749742785b8 -r 50f257ea2aba doc-src/HOL/logics-HOL.tex
--- 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}