Updated to LaTeX 2e
authorberghofe
Fri May 02 16:41:35 1997 +0200 (1997-05-02)
changeset 3098a31170b67367
parent 3097 ae362c99a635
child 3099 808681776bf7
Updated to LaTeX 2e
doc-src/Ref/Makefile
doc-src/Ref/defining.tex
doc-src/Ref/ref.rao
doc-src/Ref/ref.tex
doc-src/Ref/theory-syntax.tex
     1.1 --- a/doc-src/Ref/Makefile	Fri May 02 16:21:04 1997 +0200
     1.2 +++ b/doc-src/Ref/Makefile	Fri May 02 16:41:35 1997 +0200
     1.3 @@ -9,22 +9,22 @@
     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 -	 ../rail.sty ../proof209.sty ../iman.sty ../extra.sty
     1.8 +	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty
     1.9  
    1.10  ref.dvi.gz:   $(FILES) 
    1.11  	-rm ref.dvi*
    1.12 -	latex209 ref
    1.13 +	latex ref
    1.14  	rail ref
    1.15  	bibtex ref
    1.16 -	latex209 ref
    1.17 -	latex209 ref
    1.18 +	latex ref
    1.19 +	latex ref
    1.20  	../sedindex ref
    1.21 -	latex209 ref
    1.22 +	latex ref
    1.23  	gzip -f ref.dvi
    1.24  
    1.25  dist:   $(FILES) 
    1.26  	-rm ref.dvi*
    1.27 -	latex209 ref
    1.28 -	latex209 ref
    1.29 +	latex ref
    1.30 +	latex ref
    1.31  	../sedindex ref
    1.32 -	latex209 ref
    1.33 +	latex ref
     2.1 --- a/doc-src/Ref/defining.tex	Fri May 02 16:21:04 1997 +0200
     2.2 +++ b/doc-src/Ref/defining.tex	Fri May 02 16:41:35 1997 +0200
     2.3 @@ -469,8 +469,8 @@
     2.4  specifies no priorities.  The resulting production puts no priority
     2.5  constraints on any of its arguments and has maximal priority itself.
     2.6  Omitting priorities in this manner is prone to syntactic ambiguities unless
     2.7 -the production's right-hand side is fully bracketed, as in \verb|"if _ then _
     2.8 -else _ fi"|.
     2.9 +the production's right-hand side is fully bracketed, as in
    2.10 +\verb|"if _ then _ else _ fi"|.
    2.11  
    2.12  Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
    2.13  is sensible only if~$c$ is an identifier.  Otherwise you will be unable to
    2.14 @@ -613,8 +613,8 @@
    2.15  
    2.16  The declaration is expanded internally to something like
    2.17  \begin{ttbox}
    2.18 -\(c\)    :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
    2.19 -"\(\Q\)"\hskip-3pt  :: [idts, \(\tau@2\)] => \(\tau@3\)   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
    2.20 +\(c\)\hskip3pt    :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
    2.21 +"\(\Q\)"  :: [idts, \(\tau@2\)] => \(\tau@3\)   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
    2.22  \end{ttbox}
    2.23  Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
    2.24  \index{type constraints}
     3.1 --- a/doc-src/Ref/ref.rao	Fri May 02 16:21:04 1997 +0200
     3.2 +++ b/doc-src/Ref/ref.rao	Fri May 02 16:41:35 1997 +0200
     3.3 @@ -1,329 +1,331 @@
     3.4 -% This file was generated by 'rail' from 'ref.rai'
     3.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 }
     3.6 +% This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'ref.rai'
     3.7 +\rail@t {lbrace}
     3.8 +\rail@t {rbrace}
     3.9 +\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 | lbrace (id * ',') rbrace ; \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 }
    3.10  \rail@o {1}{
    3.11  \rail@begin{2}{theoryDef}
    3.12 -\rail@nont{id}
    3.13 -\rail@term{=}
    3.14 +\rail@nont{id}[]
    3.15 +\rail@term{=}[]
    3.16  \rail@plus
    3.17 -\rail@nont{name}
    3.18 +\rail@nont{name}[]
    3.19  \rail@nextplus{1}
    3.20 -\rail@cterm{+}
    3.21 +\rail@cterm{+}[]
    3.22  \rail@endplus
    3.23  \rail@bar
    3.24 -\rail@term{+}
    3.25 -\rail@nont{extension}
    3.26 +\rail@term{+}[]
    3.27 +\rail@nont{extension}[]
    3.28  \rail@nextbar{1}
    3.29  \rail@endbar
    3.30  \rail@end
    3.31  \rail@begin{2}{name}
    3.32  \rail@bar
    3.33 -\rail@nont{id}
    3.34 +\rail@nont{id}[]
    3.35  \rail@nextbar{1}
    3.36 -\rail@nont{string}
    3.37 +\rail@nont{string}[]
    3.38  \rail@endbar
    3.39  \rail@end
    3.40  \rail@begin{2}{extension}
    3.41  \rail@plus
    3.42 -\rail@nont{section}
    3.43 +\rail@nont{section}[]
    3.44  \rail@nextplus{1}
    3.45  \rail@endplus
    3.46 -\rail@term{end}
    3.47 +\rail@term{end}[]
    3.48  \rail@bar
    3.49  \rail@nextbar{1}
    3.50 -\rail@nont{ml}
    3.51 +\rail@nont{ml}[]
    3.52  \rail@endbar
    3.53  \rail@end
    3.54  \rail@begin{10}{section}
    3.55  \rail@bar
    3.56 -\rail@nont{classes}
    3.57 +\rail@nont{classes}[]
    3.58  \rail@nextbar{1}
    3.59 -\rail@nont{default}
    3.60 +\rail@nont{default}[]
    3.61  \rail@nextbar{2}
    3.62 -\rail@nont{types}
    3.63 +\rail@nont{types}[]
    3.64  \rail@nextbar{3}
    3.65 -\rail@nont{arities}
    3.66 +\rail@nont{arities}[]
    3.67  \rail@nextbar{4}
    3.68 -\rail@nont{consts}
    3.69 +\rail@nont{consts}[]
    3.70  \rail@nextbar{5}
    3.71 -\rail@nont{constdefs}
    3.72 +\rail@nont{constdefs}[]
    3.73  \rail@nextbar{6}
    3.74 -\rail@nont{trans}
    3.75 +\rail@nont{trans}[]
    3.76  \rail@nextbar{7}
    3.77 -\rail@nont{defs}
    3.78 +\rail@nont{defs}[]
    3.79  \rail@nextbar{8}
    3.80 -\rail@nont{rules}
    3.81 +\rail@nont{rules}[]
    3.82  \rail@nextbar{9}
    3.83 -\rail@nont{oracle}
    3.84 +\rail@nont{oracle}[]
    3.85  \rail@endbar
    3.86  \rail@end
    3.87  \rail@begin{4}{classes}
    3.88 -\rail@term{classes}
    3.89 +\rail@term{classes}[]
    3.90  \rail@plus
    3.91 -\rail@nont{id}
    3.92 +\rail@nont{id}[]
    3.93  \rail@bar
    3.94  \rail@nextbar{1}
    3.95 -\rail@term{<}
    3.96 +\rail@term{<}[]
    3.97  \rail@plus
    3.98 -\rail@nont{id}
    3.99 +\rail@nont{id}[]
   3.100  \rail@nextplus{2}
   3.101 -\rail@cterm{,}
   3.102 +\rail@cterm{,}[]
   3.103  \rail@endplus
   3.104  \rail@endbar
   3.105  \rail@nextplus{3}
   3.106  \rail@endplus
   3.107  \rail@end
   3.108  \rail@begin{1}{default}
   3.109 -\rail@term{default}
   3.110 -\rail@nont{sort}
   3.111 +\rail@term{default}[]
   3.112 +\rail@nont{sort}[]
   3.113  \rail@end
   3.114  \rail@begin{4}{sort}
   3.115  \rail@bar
   3.116 -\rail@nont{id}
   3.117 +\rail@nont{id}[]
   3.118  \rail@nextbar{1}
   3.119 -\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $}
   3.120 +\rail@token{lbrace}[]
   3.121  \rail@bar
   3.122  \rail@nextbar{2}
   3.123  \rail@plus
   3.124 -\rail@nont{id}
   3.125 +\rail@nont{id}[]
   3.126  \rail@nextplus{3}
   3.127 -\rail@cterm{,}
   3.128 +\rail@cterm{,}[]
   3.129  \rail@endplus
   3.130  \rail@endbar
   3.131 -\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $}
   3.132 +\rail@token{rbrace}[]
   3.133  \rail@endbar
   3.134  \rail@end
   3.135  \rail@begin{3}{types}
   3.136 -\rail@term{types}
   3.137 +\rail@term{types}[]
   3.138  \rail@plus
   3.139 -\rail@nont{typeDecl}
   3.140 +\rail@nont{typeDecl}[]
   3.141  \rail@bar
   3.142  \rail@nextbar{1}
   3.143 -\rail@term{(}
   3.144 -\rail@nont{infix}
   3.145 -\rail@term{)}
   3.146 +\rail@term{(}[]
   3.147 +\rail@nont{infix}[]
   3.148 +\rail@term{)}[]
   3.149  \rail@endbar
   3.150  \rail@nextplus{2}
   3.151  \rail@endplus
   3.152  \rail@end
   3.153  \rail@begin{2}{infix}
   3.154  \rail@bar
   3.155 -\rail@term{infixr}
   3.156 +\rail@term{infixr}[]
   3.157  \rail@nextbar{1}
   3.158 -\rail@term{infixl}
   3.159 +\rail@term{infixl}[]
   3.160  \rail@endbar
   3.161 -\rail@nont{nat}
   3.162 +\rail@nont{nat}[]
   3.163  \rail@end
   3.164  \rail@begin{3}{typeDecl}
   3.165 -\rail@nont{typevarlist}
   3.166 -\rail@nont{name}
   3.167 +\rail@nont{typevarlist}[]
   3.168 +\rail@nont{name}[]
   3.169  \rail@bar
   3.170  \rail@nextbar{1}
   3.171 -\rail@term{=}
   3.172 +\rail@term{=}[]
   3.173  \rail@bar
   3.174 -\rail@nont{string}
   3.175 +\rail@nont{string}[]
   3.176  \rail@nextbar{2}
   3.177 -\rail@nont{type}
   3.178 +\rail@nont{type}[]
   3.179  \rail@endbar
   3.180  \rail@endbar
   3.181  \rail@end
   3.182  \rail@begin{4}{typevarlist}
   3.183  \rail@bar
   3.184  \rail@nextbar{1}
   3.185 -\rail@nont{tid}
   3.186 +\rail@nont{tid}[]
   3.187  \rail@nextbar{2}
   3.188 -\rail@term{(}
   3.189 +\rail@term{(}[]
   3.190  \rail@plus
   3.191 -\rail@nont{tid}
   3.192 +\rail@nont{tid}[]
   3.193  \rail@nextplus{3}
   3.194 -\rail@cterm{,}
   3.195 +\rail@cterm{,}[]
   3.196  \rail@endplus
   3.197 -\rail@term{)}
   3.198 +\rail@term{)}[]
   3.199  \rail@endbar
   3.200  \rail@end
   3.201  \rail@begin{5}{type}
   3.202  \rail@bar
   3.203 -\rail@nont{simpleType}
   3.204 +\rail@nont{simpleType}[]
   3.205  \rail@nextbar{1}
   3.206 -\rail@term{(}
   3.207 -\rail@nont{type}
   3.208 -\rail@term{)}
   3.209 +\rail@term{(}[]
   3.210 +\rail@nont{type}[]
   3.211 +\rail@term{)}[]
   3.212  \rail@nextbar{2}
   3.213 -\rail@nont{type}
   3.214 -\rail@term{=>}
   3.215 -\rail@nont{type}
   3.216 +\rail@nont{type}[]
   3.217 +\rail@term{=>}[]
   3.218 +\rail@nont{type}[]
   3.219  \rail@nextbar{3}
   3.220 -\rail@term{[}
   3.221 +\rail@term{[}[]
   3.222  \rail@plus
   3.223 -\rail@nont{type}
   3.224 +\rail@nont{type}[]
   3.225  \rail@nextplus{4}
   3.226 -\rail@cterm{,}
   3.227 +\rail@cterm{,}[]
   3.228  \rail@endplus
   3.229 -\rail@term{]}
   3.230 -\rail@term{=>}
   3.231 -\rail@nont{type}
   3.232 +\rail@term{]}[]
   3.233 +\rail@term{=>}[]
   3.234 +\rail@nont{type}[]
   3.235  \rail@endbar
   3.236  \rail@end
   3.237  \rail@begin{6}{simpleType}
   3.238  \rail@bar
   3.239 -\rail@nont{id}
   3.240 +\rail@nont{id}[]
   3.241  \rail@nextbar{1}
   3.242 -\rail@nont{tid}
   3.243 +\rail@nont{tid}[]
   3.244  \rail@bar
   3.245  \rail@nextbar{2}
   3.246 -\rail@term{::}
   3.247 -\rail@nont{id}
   3.248 +\rail@term{::}[]
   3.249 +\rail@nont{id}[]
   3.250  \rail@endbar
   3.251  \rail@nextbar{3}
   3.252 -\rail@term{(}
   3.253 +\rail@term{(}[]
   3.254  \rail@plus
   3.255 -\rail@nont{type}
   3.256 +\rail@nont{type}[]
   3.257  \rail@nextplus{4}
   3.258 -\rail@cterm{,}
   3.259 +\rail@cterm{,}[]
   3.260  \rail@endplus
   3.261 -\rail@term{)}
   3.262 -\rail@nont{id}
   3.263 +\rail@term{)}[]
   3.264 +\rail@nont{id}[]
   3.265  \rail@nextbar{5}
   3.266 -\rail@nont{simpleType}
   3.267 -\rail@nont{id}
   3.268 +\rail@nont{simpleType}[]
   3.269 +\rail@nont{id}[]
   3.270  \rail@endbar
   3.271  \rail@end
   3.272  \rail@begin{3}{arities}
   3.273 -\rail@term{arities}
   3.274 +\rail@term{arities}[]
   3.275  \rail@plus
   3.276  \rail@plus
   3.277 -\rail@nont{name}
   3.278 +\rail@nont{name}[]
   3.279  \rail@nextplus{1}
   3.280 -\rail@cterm{,}
   3.281 +\rail@cterm{,}[]
   3.282  \rail@endplus
   3.283 -\rail@term{::}
   3.284 -\rail@nont{arity}
   3.285 +\rail@term{::}[]
   3.286 +\rail@nont{arity}[]
   3.287  \rail@nextplus{2}
   3.288  \rail@endplus
   3.289  \rail@end
   3.290  \rail@begin{3}{arity}
   3.291  \rail@bar
   3.292  \rail@nextbar{1}
   3.293 -\rail@term{(}
   3.294 +\rail@term{(}[]
   3.295  \rail@plus
   3.296 -\rail@nont{sort}
   3.297 +\rail@nont{sort}[]
   3.298  \rail@nextplus{2}
   3.299 -\rail@cterm{,}
   3.300 +\rail@cterm{,}[]
   3.301  \rail@endplus
   3.302 -\rail@term{)}
   3.303 +\rail@term{)}[]
   3.304  \rail@endbar
   3.305 -\rail@nont{id}
   3.306 +\rail@nont{id}[]
   3.307  \rail@end
   3.308  \rail@begin{3}{consts}
   3.309 -\rail@term{consts}
   3.310 +\rail@term{consts}[]
   3.311  \rail@plus
   3.312 -\rail@nont{constDecl}
   3.313 +\rail@nont{constDecl}[]
   3.314  \rail@bar
   3.315  \rail@nextbar{1}
   3.316 -\rail@term{(}
   3.317 -\rail@nont{mixfix}
   3.318 -\rail@term{)}
   3.319 +\rail@term{(}[]
   3.320 +\rail@nont{mixfix}[]
   3.321 +\rail@term{)}[]
   3.322  \rail@endbar
   3.323  \rail@nextplus{2}
   3.324  \rail@endplus
   3.325  \rail@end
   3.326  \rail@begin{2}{constDecl}
   3.327  \rail@plus
   3.328 -\rail@nont{name}
   3.329 +\rail@nont{name}[]
   3.330  \rail@nextplus{1}
   3.331 -\rail@cterm{,}
   3.332 +\rail@cterm{,}[]
   3.333  \rail@endplus
   3.334 -\rail@term{::}
   3.335 +\rail@term{::}[]
   3.336  \rail@bar
   3.337 -\rail@nont{string}
   3.338 +\rail@nont{string}[]
   3.339  \rail@nextbar{1}
   3.340 -\rail@nont{type}
   3.341 +\rail@nont{type}[]
   3.342  \rail@endbar
   3.343  \rail@end
   3.344  \rail@begin{6}{mixfix}
   3.345  \rail@bar
   3.346 -\rail@nont{string}
   3.347 +\rail@nont{string}[]
   3.348  \rail@bar
   3.349  \rail@nextbar{1}
   3.350  \rail@bar
   3.351  \rail@nextbar{2}
   3.352 -\rail@term{[}
   3.353 +\rail@term{[}[]
   3.354  \rail@plus
   3.355 -\rail@nont{nat}
   3.356 +\rail@nont{nat}[]
   3.357  \rail@nextplus{3}
   3.358 -\rail@cterm{,}
   3.359 +\rail@cterm{,}[]
   3.360  \rail@endplus
   3.361 -\rail@term{]}
   3.362 +\rail@term{]}[]
   3.363  \rail@endbar
   3.364 -\rail@nont{nat}
   3.365 +\rail@nont{nat}[]
   3.366  \rail@endbar
   3.367  \rail@nextbar{4}
   3.368 -\rail@nont{infix}
   3.369 +\rail@nont{infix}[]
   3.370  \rail@nextbar{5}
   3.371 -\rail@term{binder}
   3.372 -\rail@nont{string}
   3.373 -\rail@nont{nat}
   3.374 +\rail@term{binder}[]
   3.375 +\rail@nont{string}[]
   3.376 +\rail@nont{nat}[]
   3.377  \rail@endbar
   3.378  \rail@end
   3.379  \rail@begin{3}{constdefs}
   3.380 -\rail@term{constdefs}
   3.381 +\rail@term{constdefs}[]
   3.382  \rail@plus
   3.383 -\rail@nont{id}
   3.384 -\rail@term{::}
   3.385 +\rail@nont{id}[]
   3.386 +\rail@term{::}[]
   3.387  \rail@bar
   3.388 -\rail@nont{string}
   3.389 +\rail@nont{string}[]
   3.390  \rail@nextbar{1}
   3.391 -\rail@nont{type}
   3.392 +\rail@nont{type}[]
   3.393  \rail@endbar
   3.394 -\rail@nont{string}
   3.395 +\rail@nont{string}[]
   3.396  \rail@nextplus{2}
   3.397  \rail@endplus
   3.398  \rail@end
   3.399  \rail@begin{4}{trans}
   3.400 -\rail@term{translations}
   3.401 +\rail@term{translations}[]
   3.402  \rail@plus
   3.403 -\rail@nont{pat}
   3.404 +\rail@nont{pat}[]
   3.405  \rail@bar
   3.406 -\rail@term{==}
   3.407 +\rail@term{==}[]
   3.408  \rail@nextbar{1}
   3.409 -\rail@term{=>}
   3.410 +\rail@term{=>}[]
   3.411  \rail@nextbar{2}
   3.412 -\rail@term{<=}
   3.413 +\rail@term{<=}[]
   3.414  \rail@endbar
   3.415 -\rail@nont{pat}
   3.416 +\rail@nont{pat}[]
   3.417  \rail@nextplus{3}
   3.418  \rail@endplus
   3.419  \rail@end
   3.420  \rail@begin{2}{pat}
   3.421  \rail@bar
   3.422  \rail@nextbar{1}
   3.423 -\rail@term{(}
   3.424 -\rail@nont{id}
   3.425 -\rail@term{)}
   3.426 +\rail@term{(}[]
   3.427 +\rail@nont{id}[]
   3.428 +\rail@term{)}[]
   3.429  \rail@endbar
   3.430 -\rail@nont{string}
   3.431 +\rail@nont{string}[]
   3.432  \rail@end
   3.433  \rail@begin{2}{rules}
   3.434 -\rail@term{rules}
   3.435 +\rail@term{rules}[]
   3.436  \rail@plus
   3.437 -\rail@nont{id}
   3.438 -\rail@nont{string}
   3.439 +\rail@nont{id}[]
   3.440 +\rail@nont{string}[]
   3.441  \rail@nextplus{1}
   3.442  \rail@endplus
   3.443  \rail@end
   3.444  \rail@begin{2}{defs}
   3.445 -\rail@term{defs}
   3.446 +\rail@term{defs}[]
   3.447  \rail@plus
   3.448 -\rail@nont{id}
   3.449 -\rail@nont{string}
   3.450 +\rail@nont{id}[]
   3.451 +\rail@nont{string}[]
   3.452  \rail@nextplus{1}
   3.453  \rail@endplus
   3.454  \rail@end
   3.455  \rail@begin{1}{oracle}
   3.456 -\rail@term{oracle}
   3.457 -\rail@nont{name}
   3.458 +\rail@term{oracle}[]
   3.459 +\rail@nont{name}[]
   3.460  \rail@end
   3.461  \rail@begin{1}{ml}
   3.462 -\rail@term{ML}
   3.463 -\rail@nont{text}
   3.464 +\rail@term{ML}[]
   3.465 +\rail@nont{text}[]
   3.466  \rail@end
   3.467  }
     4.1 --- a/doc-src/Ref/ref.tex	Fri May 02 16:21:04 1997 +0200
     4.2 +++ b/doc-src/Ref/ref.tex	Fri May 02 16:41:35 1997 +0200
     4.3 @@ -1,7 +1,9 @@
     4.4 -\documentstyle[a4,12pt]{report}
     4.5 +\documentclass[12pt]{report}
     4.6 +\usepackage{a4}
     4.7 +
     4.8  \makeatletter
     4.9  \input{../rail.sty}
    4.10 -\input{../proof209.sty}
    4.11 +\input{../proof.sty}
    4.12  \input{../iman.sty}
    4.13  \input{../extra.sty}
    4.14  \makeatother
    4.15 @@ -38,6 +40,10 @@
    4.16  \sloppy
    4.17  \binperiod     %%%treat . like a binary operator
    4.18  
    4.19 +\railalias{lbrace}{\{}
    4.20 +\railalias{rbrace}{\}}
    4.21 +\railterm{lbrace,rbrace}
    4.22 +
    4.23  \begin{document}
    4.24  \index{definitions|see{rewriting, meta-level}}
    4.25  \index{rewriting!object-level|see{simplification}}
     5.1 --- a/doc-src/Ref/theory-syntax.tex	Fri May 02 16:21:04 1997 +0200
     5.2 +++ b/doc-src/Ref/theory-syntax.tex	Fri May 02 16:41:35 1997 +0200
     5.3 @@ -49,7 +49,7 @@
     5.4          ;
     5.5  
     5.6  sort :  id
     5.7 -     | '\{' (id * ',') '\}'
     5.8 +     | lbrace (id * ',') rbrace
     5.9       ;
    5.10  
    5.11  types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )