rail output;
authorwenzelm
Thu Feb 20 15:13:52 1997 +0100 (1997-02-20)
changeset 2657448bb82c4003
parent 2656 71097a167f0b
child 2658 13ba951a4572
rail output;
doc-src/Ref/Makefile
doc-src/Ref/ref.rao
doc-src/Ref/ref.tex
     1.1 --- a/doc-src/Ref/Makefile	Thu Feb 20 14:59:02 1997 +0100
     1.2 +++ b/doc-src/Ref/Makefile	Thu Feb 20 15:13:52 1997 +0100
     1.3 @@ -9,10 +9,10 @@
     1.4  FILES =  ref.tex introduction.tex goals.tex tactic.tex tctical.tex\
     1.5           thm.tex theories.tex defining.tex syntax.tex substitution.tex\
     1.6           simplifier.tex classical.tex theory-syntax.tex\
     1.7 -	 ../iman.sty ../extra.sty
     1.8 +	 ../proof209.sty ../iman.sty ../extra.sty
     1.9  
    1.10  ref.dvi.gz:   $(FILES) 
    1.11 -	-rm ref.dvi.gz
    1.12 +	-rm ref.dvi*
    1.13  	latex209 ref
    1.14  	rail ref
    1.15  	bibtex ref
    1.16 @@ -21,3 +21,10 @@
    1.17  	../sedindex ref
    1.18  	latex209 ref
    1.19  	gzip -f ref.dvi
    1.20 +
    1.21 +dist:   $(FILES) 
    1.22 +	-rm ref.dvi*
    1.23 +	latex209 ref
    1.24 +	latex209 ref
    1.25 +	../sedindex ref
    1.26 +	latex209 ref
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/Ref/ref.rao	Thu Feb 20 15:13:52 1997 +0100
     2.3 @@ -0,0 +1,329 @@
     2.4 +% This file was generated by 'rail' from 'ref.rai'
     2.5 +\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()); \par name: id | string; \par extension : (section +) 'end' ( () | ml ); \par section : classes | default | types | arities | consts | constdefs | trans | defs | rules | oracle ; \par classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; \par default : 'default' sort ; \par sort : id | '\protect \relax $\mathsurround =\z@ \delimiter "4266308 $' (id * ',') '\protect \relax $\mathsurround =\z@ \delimiter "5267309 $' ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id; \par \par arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; \par arity : ( () | '(' (sort + ',') ')' ) id ; \par \par consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
     2.6 +\rail@o {1}{
     2.7 +\rail@begin{2}{theoryDef}
     2.8 +\rail@nont{id}
     2.9 +\rail@term{=}
    2.10 +\rail@plus
    2.11 +\rail@nont{name}
    2.12 +\rail@nextplus{1}
    2.13 +\rail@cterm{+}
    2.14 +\rail@endplus
    2.15 +\rail@bar
    2.16 +\rail@term{+}
    2.17 +\rail@nont{extension}
    2.18 +\rail@nextbar{1}
    2.19 +\rail@endbar
    2.20 +\rail@end
    2.21 +\rail@begin{2}{name}
    2.22 +\rail@bar
    2.23 +\rail@nont{id}
    2.24 +\rail@nextbar{1}
    2.25 +\rail@nont{string}
    2.26 +\rail@endbar
    2.27 +\rail@end
    2.28 +\rail@begin{2}{extension}
    2.29 +\rail@plus
    2.30 +\rail@nont{section}
    2.31 +\rail@nextplus{1}
    2.32 +\rail@endplus
    2.33 +\rail@term{end}
    2.34 +\rail@bar
    2.35 +\rail@nextbar{1}
    2.36 +\rail@nont{ml}
    2.37 +\rail@endbar
    2.38 +\rail@end
    2.39 +\rail@begin{10}{section}
    2.40 +\rail@bar
    2.41 +\rail@nont{classes}
    2.42 +\rail@nextbar{1}
    2.43 +\rail@nont{default}
    2.44 +\rail@nextbar{2}
    2.45 +\rail@nont{types}
    2.46 +\rail@nextbar{3}
    2.47 +\rail@nont{arities}
    2.48 +\rail@nextbar{4}
    2.49 +\rail@nont{consts}
    2.50 +\rail@nextbar{5}
    2.51 +\rail@nont{constdefs}
    2.52 +\rail@nextbar{6}
    2.53 +\rail@nont{trans}
    2.54 +\rail@nextbar{7}
    2.55 +\rail@nont{defs}
    2.56 +\rail@nextbar{8}
    2.57 +\rail@nont{rules}
    2.58 +\rail@nextbar{9}
    2.59 +\rail@nont{oracle}
    2.60 +\rail@endbar
    2.61 +\rail@end
    2.62 +\rail@begin{4}{classes}
    2.63 +\rail@term{classes}
    2.64 +\rail@plus
    2.65 +\rail@nont{id}
    2.66 +\rail@bar
    2.67 +\rail@nextbar{1}
    2.68 +\rail@term{<}
    2.69 +\rail@plus
    2.70 +\rail@nont{id}
    2.71 +\rail@nextplus{2}
    2.72 +\rail@cterm{,}
    2.73 +\rail@endplus
    2.74 +\rail@endbar
    2.75 +\rail@nextplus{3}
    2.76 +\rail@endplus
    2.77 +\rail@end
    2.78 +\rail@begin{1}{default}
    2.79 +\rail@term{default}
    2.80 +\rail@nont{sort}
    2.81 +\rail@end
    2.82 +\rail@begin{4}{sort}
    2.83 +\rail@bar
    2.84 +\rail@nont{id}
    2.85 +\rail@nextbar{1}
    2.86 +\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $}
    2.87 +\rail@bar
    2.88 +\rail@nextbar{2}
    2.89 +\rail@plus
    2.90 +\rail@nont{id}
    2.91 +\rail@nextplus{3}
    2.92 +\rail@cterm{,}
    2.93 +\rail@endplus
    2.94 +\rail@endbar
    2.95 +\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $}
    2.96 +\rail@endbar
    2.97 +\rail@end
    2.98 +\rail@begin{3}{types}
    2.99 +\rail@term{types}
   2.100 +\rail@plus
   2.101 +\rail@nont{typeDecl}
   2.102 +\rail@bar
   2.103 +\rail@nextbar{1}
   2.104 +\rail@term{(}
   2.105 +\rail@nont{infix}
   2.106 +\rail@term{)}
   2.107 +\rail@endbar
   2.108 +\rail@nextplus{2}
   2.109 +\rail@endplus
   2.110 +\rail@end
   2.111 +\rail@begin{2}{infix}
   2.112 +\rail@bar
   2.113 +\rail@term{infixr}
   2.114 +\rail@nextbar{1}
   2.115 +\rail@term{infixl}
   2.116 +\rail@endbar
   2.117 +\rail@nont{nat}
   2.118 +\rail@end
   2.119 +\rail@begin{3}{typeDecl}
   2.120 +\rail@nont{typevarlist}
   2.121 +\rail@nont{name}
   2.122 +\rail@bar
   2.123 +\rail@nextbar{1}
   2.124 +\rail@term{=}
   2.125 +\rail@bar
   2.126 +\rail@nont{string}
   2.127 +\rail@nextbar{2}
   2.128 +\rail@nont{type}
   2.129 +\rail@endbar
   2.130 +\rail@endbar
   2.131 +\rail@end
   2.132 +\rail@begin{4}{typevarlist}
   2.133 +\rail@bar
   2.134 +\rail@nextbar{1}
   2.135 +\rail@nont{tid}
   2.136 +\rail@nextbar{2}
   2.137 +\rail@term{(}
   2.138 +\rail@plus
   2.139 +\rail@nont{tid}
   2.140 +\rail@nextplus{3}
   2.141 +\rail@cterm{,}
   2.142 +\rail@endplus
   2.143 +\rail@term{)}
   2.144 +\rail@endbar
   2.145 +\rail@end
   2.146 +\rail@begin{5}{type}
   2.147 +\rail@bar
   2.148 +\rail@nont{simpleType}
   2.149 +\rail@nextbar{1}
   2.150 +\rail@term{(}
   2.151 +\rail@nont{type}
   2.152 +\rail@term{)}
   2.153 +\rail@nextbar{2}
   2.154 +\rail@nont{type}
   2.155 +\rail@term{=>}
   2.156 +\rail@nont{type}
   2.157 +\rail@nextbar{3}
   2.158 +\rail@term{[}
   2.159 +\rail@plus
   2.160 +\rail@nont{type}
   2.161 +\rail@nextplus{4}
   2.162 +\rail@cterm{,}
   2.163 +\rail@endplus
   2.164 +\rail@term{]}
   2.165 +\rail@term{=>}
   2.166 +\rail@nont{type}
   2.167 +\rail@endbar
   2.168 +\rail@end
   2.169 +\rail@begin{6}{simpleType}
   2.170 +\rail@bar
   2.171 +\rail@nont{id}
   2.172 +\rail@nextbar{1}
   2.173 +\rail@nont{tid}
   2.174 +\rail@bar
   2.175 +\rail@nextbar{2}
   2.176 +\rail@term{::}
   2.177 +\rail@nont{id}
   2.178 +\rail@endbar
   2.179 +\rail@nextbar{3}
   2.180 +\rail@term{(}
   2.181 +\rail@plus
   2.182 +\rail@nont{type}
   2.183 +\rail@nextplus{4}
   2.184 +\rail@cterm{,}
   2.185 +\rail@endplus
   2.186 +\rail@term{)}
   2.187 +\rail@nont{id}
   2.188 +\rail@nextbar{5}
   2.189 +\rail@nont{simpleType}
   2.190 +\rail@nont{id}
   2.191 +\rail@endbar
   2.192 +\rail@end
   2.193 +\rail@begin{3}{arities}
   2.194 +\rail@term{arities}
   2.195 +\rail@plus
   2.196 +\rail@plus
   2.197 +\rail@nont{name}
   2.198 +\rail@nextplus{1}
   2.199 +\rail@cterm{,}
   2.200 +\rail@endplus
   2.201 +\rail@term{::}
   2.202 +\rail@nont{arity}
   2.203 +\rail@nextplus{2}
   2.204 +\rail@endplus
   2.205 +\rail@end
   2.206 +\rail@begin{3}{arity}
   2.207 +\rail@bar
   2.208 +\rail@nextbar{1}
   2.209 +\rail@term{(}
   2.210 +\rail@plus
   2.211 +\rail@nont{sort}
   2.212 +\rail@nextplus{2}
   2.213 +\rail@cterm{,}
   2.214 +\rail@endplus
   2.215 +\rail@term{)}
   2.216 +\rail@endbar
   2.217 +\rail@nont{id}
   2.218 +\rail@end
   2.219 +\rail@begin{3}{consts}
   2.220 +\rail@term{consts}
   2.221 +\rail@plus
   2.222 +\rail@nont{constDecl}
   2.223 +\rail@bar
   2.224 +\rail@nextbar{1}
   2.225 +\rail@term{(}
   2.226 +\rail@nont{mixfix}
   2.227 +\rail@term{)}
   2.228 +\rail@endbar
   2.229 +\rail@nextplus{2}
   2.230 +\rail@endplus
   2.231 +\rail@end
   2.232 +\rail@begin{2}{constDecl}
   2.233 +\rail@plus
   2.234 +\rail@nont{name}
   2.235 +\rail@nextplus{1}
   2.236 +\rail@cterm{,}
   2.237 +\rail@endplus
   2.238 +\rail@term{::}
   2.239 +\rail@bar
   2.240 +\rail@nont{string}
   2.241 +\rail@nextbar{1}
   2.242 +\rail@nont{type}
   2.243 +\rail@endbar
   2.244 +\rail@end
   2.245 +\rail@begin{6}{mixfix}
   2.246 +\rail@bar
   2.247 +\rail@nont{string}
   2.248 +\rail@bar
   2.249 +\rail@nextbar{1}
   2.250 +\rail@bar
   2.251 +\rail@nextbar{2}
   2.252 +\rail@term{[}
   2.253 +\rail@plus
   2.254 +\rail@nont{nat}
   2.255 +\rail@nextplus{3}
   2.256 +\rail@cterm{,}
   2.257 +\rail@endplus
   2.258 +\rail@term{]}
   2.259 +\rail@endbar
   2.260 +\rail@nont{nat}
   2.261 +\rail@endbar
   2.262 +\rail@nextbar{4}
   2.263 +\rail@nont{infix}
   2.264 +\rail@nextbar{5}
   2.265 +\rail@term{binder}
   2.266 +\rail@nont{string}
   2.267 +\rail@nont{nat}
   2.268 +\rail@endbar
   2.269 +\rail@end
   2.270 +\rail@begin{3}{constdefs}
   2.271 +\rail@term{constdefs}
   2.272 +\rail@plus
   2.273 +\rail@nont{id}
   2.274 +\rail@term{::}
   2.275 +\rail@bar
   2.276 +\rail@nont{string}
   2.277 +\rail@nextbar{1}
   2.278 +\rail@nont{type}
   2.279 +\rail@endbar
   2.280 +\rail@nont{string}
   2.281 +\rail@nextplus{2}
   2.282 +\rail@endplus
   2.283 +\rail@end
   2.284 +\rail@begin{4}{trans}
   2.285 +\rail@term{translations}
   2.286 +\rail@plus
   2.287 +\rail@nont{pat}
   2.288 +\rail@bar
   2.289 +\rail@term{==}
   2.290 +\rail@nextbar{1}
   2.291 +\rail@term{=>}
   2.292 +\rail@nextbar{2}
   2.293 +\rail@term{<=}
   2.294 +\rail@endbar
   2.295 +\rail@nont{pat}
   2.296 +\rail@nextplus{3}
   2.297 +\rail@endplus
   2.298 +\rail@end
   2.299 +\rail@begin{2}{pat}
   2.300 +\rail@bar
   2.301 +\rail@nextbar{1}
   2.302 +\rail@term{(}
   2.303 +\rail@nont{id}
   2.304 +\rail@term{)}
   2.305 +\rail@endbar
   2.306 +\rail@nont{string}
   2.307 +\rail@end
   2.308 +\rail@begin{2}{rules}
   2.309 +\rail@term{rules}
   2.310 +\rail@plus
   2.311 +\rail@nont{id}
   2.312 +\rail@nont{string}
   2.313 +\rail@nextplus{1}
   2.314 +\rail@endplus
   2.315 +\rail@end
   2.316 +\rail@begin{2}{defs}
   2.317 +\rail@term{defs}
   2.318 +\rail@plus
   2.319 +\rail@nont{id}
   2.320 +\rail@nont{string}
   2.321 +\rail@nextplus{1}
   2.322 +\rail@endplus
   2.323 +\rail@end
   2.324 +\rail@begin{1}{oracle}
   2.325 +\rail@term{oracle}
   2.326 +\rail@nont{name}
   2.327 +\rail@end
   2.328 +\rail@begin{1}{ml}
   2.329 +\rail@term{ML}
   2.330 +\rail@nont{text}
   2.331 +\rail@end
   2.332 +}
     3.1 --- a/doc-src/Ref/ref.tex	Thu Feb 20 14:59:02 1997 +0100
     3.2 +++ b/doc-src/Ref/ref.tex	Thu Feb 20 15:13:52 1997 +0100
     3.3 @@ -1,4 +1,10 @@
     3.4 -\documentstyle[a4,12pt,rail,proof209,iman,extra]{report}
     3.5 +\documentstyle[a4,12pt,rail]{report}
     3.6 +\makeatletter
     3.7 +\input{../proof209.sty}
     3.8 +\input{../iman.sty}
     3.9 +\input{../extra.sty}
    3.10 +\makeatother
    3.11 +
    3.12  %% $Id$
    3.13  %%\includeonly{}
    3.14  %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}