# HG changeset patch
# User wenzelm
# Date 1304349131 -7200
# Node ID 9691759a9b3c3ce2ba4868abadd547ae0d35df43
# Parent  a38e0f15d76579afad497b9d774c00138a1c7673
removed obsolete rail diagram (which was about old-style theory syntax);

diff -r a38e0f15d765 -r 9691759a9b3c doc-src/ZF/Makefile
--- a/doc-src/ZF/Makefile	Mon May 02 17:07:46 2011 +0200
+++ b/doc-src/ZF/Makefile	Mon May 02 17:12:11 2011 +0200
@@ -16,9 +16,6 @@
   ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty	\
   ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty ../manual.bib
 
-rail:
-	$(RAIL) $(NAME)
-
 dvi: $(NAME).dvi
 
 $(NAME).dvi: $(FILES) isabelle_zf.eps
diff -r a38e0f15d765 -r 9691759a9b3c doc-src/ZF/ZF.tex
--- a/doc-src/ZF/ZF.tex	Mon May 02 17:07:46 2011 +0200
+++ b/doc-src/ZF/ZF.tex	Mon May 02 17:12:11 2011 +0200
@@ -1761,27 +1761,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.  The quotation marks are necessary because
-they enclose general Isabelle formul\ae.
-
-\begin{figure}
-\begin{rail}
-datatype : ( 'datatype' | 'codatatype' ) datadecls;
-
-datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and'
-         ;
-constructor : name ( () | consargs )  ( () | ( '(' mixfix ')' ) )
-         ;
-consargs : '(' ('"' var ' : ' term '"' + ',') ')'
-         ;
-\end{rail}
-\caption{Syntax of datatype declarations}
-\label{datatype-grammar}
-\end{figure}
+The theory syntax for datatype definitions is shown 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.
 
 Codatatypes are declared like datatypes and are identical to them in every
 respect except that they have a coinduction rule instead of an induction rule.