1.1 --- a/doc-src/ZF/Makefile	Mon May 02 17:28:45 2011 +0200
     1.2 +++ b/doc-src/ZF/Makefile	Mon May 02 17:43:06 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  NAME = logics-ZF
     1.6  FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex logics.sty	\
     1.7 -  ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty	\
     1.8 +  ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty	\
     1.9    ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty ../manual.bib
    1.10  
    1.11  dvi: $(NAME).dvi

     2.1 --- a/doc-src/ZF/logics-ZF.rai	Mon May 02 17:28:45 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,2 +0,0 @@
     2.4 -\rail@i{1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
     2.5 -datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }

     3.1 --- a/doc-src/ZF/logics-ZF.rao	Mon May 02 17:28:45 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,55 +0,0 @@
     3.4 -% This file was generated by 'rail' from 'logics-ZF.rai'
     3.5 -\rail@i {1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
     3.6 -datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
     3.7 -\rail@o {1}{
     3.8 -\rail@begin{2}{datatype}
     3.9 -\rail@bar
    3.10 -\rail@term{datatype}[]
    3.11 -\rail@nextbar{1}
    3.12 -\rail@term{codatatype}[]
    3.13 -\rail@endbar
    3.14 -\rail@nont{datadecls}[]
    3.15 -\rail@end
    3.16 -\rail@begin{3}{datadecls}
    3.17 -\rail@plus
    3.18 -\rail@term{"}[]
    3.19 -\rail@nont{id}[]
    3.20 -\rail@nont{arglist}[]
    3.21 -\rail@term{"}[]
    3.22 -\rail@term{=}[]
    3.23 -\rail@plus
    3.24 -\rail@nont{constructor}[]
    3.25 -\rail@nextplus{1}
    3.26 -\rail@cterm{|}[]
    3.27 -\rail@endplus
    3.28 -\rail@nextplus{2}
    3.29 -\rail@cterm{and}[]
    3.30 -\rail@endplus
    3.31 -\rail@end
    3.32 -\rail@begin{2}{constructor}
    3.33 -\rail@nont{name}[]
    3.34 -\rail@bar
    3.35 -\rail@nextbar{1}
    3.36 -\rail@nont{consargs}[]
    3.37 -\rail@endbar
    3.38 -\rail@bar
    3.39 -\rail@nextbar{1}
    3.40 -\rail@term{(}[]
    3.41 -\rail@nont{mixfix}[]
    3.42 -\rail@term{)}[]
    3.43 -\rail@endbar
    3.44 -\rail@end
    3.45 -\rail@begin{2}{consargs}
    3.46 -\rail@term{(}[]
    3.47 -\rail@plus
    3.48 -\rail@term{"}[]
    3.49 -\rail@nont{var}[]
    3.50 -\rail@term{ : }[]
    3.51 -\rail@nont{term}[]
    3.52 -\rail@term{"}[]
    3.53 -\rail@nextplus{1}
    3.54 -\rail@cterm{,}[]
    3.55 -\rail@endplus
    3.56 -\rail@term{)}[]
    3.57 -\rail@end
    3.58 -}

     4.1 --- a/doc-src/ZF/logics-ZF.tex	Mon May 02 17:28:45 2011 +0200
     4.2 +++ b/doc-src/ZF/logics-ZF.tex	Mon May 02 17:43:06 2011 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  %% $Id$
     4.5  \documentclass[11pt,a4paper]{report}
     4.6  \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     4.7 -\usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}
     4.8 +\usepackage{graphicx,logics,../ttbox,../proof,latexsym}
     4.9  
    4.10  \usepackage{../pdfsetup}   
    4.11  %last package!