# HG changeset patch
# User wenzelm
# Date 1304265329 -7200
# Node ID 57367832b81ad3c33424e34ea5af0fd59ac58fb4
# Parent  b68e1c27709a47b5f7d7feafa24a04008c3063fa
include static rail files for old manuals, to make standard make job independent of the "rail" executable;

diff -r b68e1c27709a -r 57367832b81a .hgignore
--- a/.hgignore	Sun May 01 17:42:21 2011 +0200
+++ b/.hgignore	Sun May 01 17:55:29 2011 +0200
@@ -20,8 +20,6 @@
 ^doc-src/.*\.lof
 ^doc-src/.*\.log
 ^doc-src/.*\.out
-^doc-src/.*\.rai
-^doc-src/.*\.rao
 ^doc-src/.*\.toc
 
 ^src/Tools/jEdit/nbproject/private/
diff -r b68e1c27709a -r 57367832b81a doc-src/HOL/Makefile
--- a/doc-src/HOL/Makefile	Sun May 01 17:42:21 2011 +0200
+++ b/doc-src/HOL/Makefile	Sun May 01 17:55:29 2011 +0200
@@ -15,11 +15,13 @@
 FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \
 	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
 
+rail:
+	$(RAIL) $(NAME)
+
 dvi: $(NAME).dvi
 
 $(NAME).dvi: $(FILES) isabelle_hol.eps
 	$(LATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -30,7 +32,6 @@
 
 $(NAME).pdf: $(FILES) isabelle_hol.pdf
 	$(PDFLATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
diff -r b68e1c27709a -r 57367832b81a doc-src/HOL/logics-HOL.rai
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/HOL/logics-HOL.rai	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,15 @@
+\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 ')') ; }
+\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@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; }
diff -r b68e1c27709a -r 57367832b81a doc-src/HOL/logics-HOL.rao
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/HOL/logics-HOL.rao	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,210 @@
+% 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 b68e1c27709a -r 57367832b81a doc-src/HOL/logics-HOL.tex
--- a/doc-src/HOL/logics-HOL.tex	Sun May 01 17:42:21 2011 +0200
+++ b/doc-src/HOL/logics-HOL.tex	Sun May 01 17:55:29 2011 +0200
@@ -1,5 +1,6 @@
 %% $Id$
 \documentclass[12pt,a4paper]{report}
+\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
 \usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,latexsym,../pdfsetup}
 
 %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
diff -r b68e1c27709a -r 57367832b81a doc-src/ZF/Makefile
--- a/doc-src/ZF/Makefile	Sun May 01 17:42:21 2011 +0200
+++ b/doc-src/ZF/Makefile	Sun May 01 17:55:29 2011 +0200
@@ -16,11 +16,13 @@
   ../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
 	$(LATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -31,7 +33,6 @@
 
 $(NAME).pdf: $(FILES) isabelle_zf.pdf
 	$(PDFLATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
diff -r b68e1c27709a -r 57367832b81a doc-src/ZF/logics-ZF.rai
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/logics-ZF.rai	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,2 @@
+\rail@i{1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
+datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
diff -r b68e1c27709a -r 57367832b81a doc-src/ZF/logics-ZF.rao
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/logics-ZF.rao	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,55 @@
+% This file was generated by 'rail' from 'logics-ZF.rai'
+\rail@i {1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par
+datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ' : ' term '"' + ',') ')' ; }
+\rail@o {1}{
+\rail@begin{2}{datatype}
+\rail@bar
+\rail@term{datatype}[]
+\rail@nextbar{1}
+\rail@term{codatatype}[]
+\rail@endbar
+\rail@nont{datadecls}[]
+\rail@end
+\rail@begin{3}{datadecls}
+\rail@plus
+\rail@term{"}[]
+\rail@nont{id}[]
+\rail@nont{arglist}[]
+\rail@term{"}[]
+\rail@term{=}[]
+\rail@plus
+\rail@nont{constructor}[]
+\rail@nextplus{1}
+\rail@cterm{|}[]
+\rail@endplus
+\rail@nextplus{2}
+\rail@cterm{and}[]
+\rail@endplus
+\rail@end
+\rail@begin{2}{constructor}
+\rail@nont{name}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{consargs}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{mixfix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{consargs}
+\rail@term{(}[]
+\rail@plus
+\rail@term{"}[]
+\rail@nont{var}[]
+\rail@term{ : }[]
+\rail@nont{term}[]
+\rail@term{"}[]
+\rail@nextplus{1}
+\rail@cterm{,}[]
+\rail@endplus
+\rail@term{)}[]
+\rail@end
+}