diff -r ae362c99a635 -r a31170b67367 doc-src/Ref/ref.rao
--- a/doc-src/Ref/ref.rao	Fri May 02 16:21:04 1997 +0200
+++ b/doc-src/Ref/ref.rao	Fri May 02 16:41:35 1997 +0200
@@ -1,329 +1,331 @@
-% This file was generated by 'rail' from 'ref.rai'
-\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 }
+% This file was generated by '/usr/stud/berghofe/latex/rail/rail' from 'ref.rai'
+\rail@t {lbrace}
+\rail@t {rbrace}
+\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 }
 \rail@o {1}{
 \rail@begin{2}{theoryDef}
-\rail@nont{id}
-\rail@term{=}
+\rail@nont{id}[]
+\rail@term{=}[]
 \rail@plus
-\rail@nont{name}
+\rail@nont{name}[]
 \rail@nextplus{1}
-\rail@cterm{+}
+\rail@cterm{+}[]
 \rail@endplus
 \rail@bar
-\rail@term{+}
-\rail@nont{extension}
+\rail@term{+}[]
+\rail@nont{extension}[]
 \rail@nextbar{1}
 \rail@endbar
 \rail@end
 \rail@begin{2}{name}
 \rail@bar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextbar{1}
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@endbar
 \rail@end
 \rail@begin{2}{extension}
 \rail@plus
-\rail@nont{section}
+\rail@nont{section}[]
 \rail@nextplus{1}
 \rail@endplus
-\rail@term{end}
+\rail@term{end}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{ml}
+\rail@nont{ml}[]
 \rail@endbar
 \rail@end
 \rail@begin{10}{section}
 \rail@bar
-\rail@nont{classes}
+\rail@nont{classes}[]
 \rail@nextbar{1}
-\rail@nont{default}
+\rail@nont{default}[]
 \rail@nextbar{2}
-\rail@nont{types}
+\rail@nont{types}[]
 \rail@nextbar{3}
-\rail@nont{arities}
+\rail@nont{arities}[]
 \rail@nextbar{4}
-\rail@nont{consts}
+\rail@nont{consts}[]
 \rail@nextbar{5}
-\rail@nont{constdefs}
+\rail@nont{constdefs}[]
 \rail@nextbar{6}
-\rail@nont{trans}
+\rail@nont{trans}[]
 \rail@nextbar{7}
-\rail@nont{defs}
+\rail@nont{defs}[]
 \rail@nextbar{8}
-\rail@nont{rules}
+\rail@nont{rules}[]
 \rail@nextbar{9}
-\rail@nont{oracle}
+\rail@nont{oracle}[]
 \rail@endbar
 \rail@end
 \rail@begin{4}{classes}
-\rail@term{classes}
+\rail@term{classes}[]
 \rail@plus
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{<}
+\rail@term{<}[]
 \rail@plus
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextplus{2}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
 \rail@endbar
 \rail@nextplus{3}
 \rail@endplus
 \rail@end
 \rail@begin{1}{default}
-\rail@term{default}
-\rail@nont{sort}
+\rail@term{default}[]
+\rail@nont{sort}[]
 \rail@end
 \rail@begin{4}{sort}
 \rail@bar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextbar{1}
-\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $}
+\rail@token{lbrace}[]
 \rail@bar
 \rail@nextbar{2}
 \rail@plus
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextplus{3}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
 \rail@endbar
-\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $}
+\rail@token{rbrace}[]
 \rail@endbar
 \rail@end
 \rail@begin{3}{types}
-\rail@term{types}
+\rail@term{types}[]
 \rail@plus
-\rail@nont{typeDecl}
+\rail@nont{typeDecl}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{infix}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{infix}[]
+\rail@term{)}[]
 \rail@endbar
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{2}{infix}
 \rail@bar
-\rail@term{infixr}
+\rail@term{infixr}[]
 \rail@nextbar{1}
-\rail@term{infixl}
+\rail@term{infixl}[]
 \rail@endbar
-\rail@nont{nat}
+\rail@nont{nat}[]
 \rail@end
 \rail@begin{3}{typeDecl}
-\rail@nont{typevarlist}
-\rail@nont{name}
+\rail@nont{typevarlist}[]
+\rail@nont{name}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{=}
+\rail@term{=}[]
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextbar{2}
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@endbar
 \rail@endbar
 \rail@end
 \rail@begin{4}{typevarlist}
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{tid}
+\rail@nont{tid}[]
 \rail@nextbar{2}
-\rail@term{(}
+\rail@term{(}[]
 \rail@plus
-\rail@nont{tid}
+\rail@nont{tid}[]
 \rail@nextplus{3}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{)}
+\rail@term{)}[]
 \rail@endbar
 \rail@end
 \rail@begin{5}{type}
 \rail@bar
-\rail@nont{simpleType}
+\rail@nont{simpleType}[]
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{type}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{type}[]
+\rail@term{)}[]
 \rail@nextbar{2}
-\rail@nont{type}
-\rail@term{=>}
-\rail@nont{type}
+\rail@nont{type}[]
+\rail@term{=>}[]
+\rail@nont{type}[]
 \rail@nextbar{3}
-\rail@term{[}
+\rail@term{[}[]
 \rail@plus
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@nextplus{4}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{]}
-\rail@term{=>}
-\rail@nont{type}
+\rail@term{]}[]
+\rail@term{=>}[]
+\rail@nont{type}[]
 \rail@endbar
 \rail@end
 \rail@begin{6}{simpleType}
 \rail@bar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@nextbar{1}
-\rail@nont{tid}
+\rail@nont{tid}[]
 \rail@bar
 \rail@nextbar{2}
-\rail@term{::}
-\rail@nont{id}
+\rail@term{::}[]
+\rail@nont{id}[]
 \rail@endbar
 \rail@nextbar{3}
-\rail@term{(}
+\rail@term{(}[]
 \rail@plus
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@nextplus{4}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{)}
-\rail@nont{id}
+\rail@term{)}[]
+\rail@nont{id}[]
 \rail@nextbar{5}
-\rail@nont{simpleType}
-\rail@nont{id}
+\rail@nont{simpleType}[]
+\rail@nont{id}[]
 \rail@endbar
 \rail@end
 \rail@begin{3}{arities}
-\rail@term{arities}
+\rail@term{arities}[]
 \rail@plus
 \rail@plus
-\rail@nont{name}
+\rail@nont{name}[]
 \rail@nextplus{1}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{::}
-\rail@nont{arity}
+\rail@term{::}[]
+\rail@nont{arity}[]
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{3}{arity}
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
+\rail@term{(}[]
 \rail@plus
-\rail@nont{sort}
+\rail@nont{sort}[]
 \rail@nextplus{2}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{)}
+\rail@term{)}[]
 \rail@endbar
-\rail@nont{id}
+\rail@nont{id}[]
 \rail@end
 \rail@begin{3}{consts}
-\rail@term{consts}
+\rail@term{consts}[]
 \rail@plus
-\rail@nont{constDecl}
+\rail@nont{constDecl}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{mixfix}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{mixfix}[]
+\rail@term{)}[]
 \rail@endbar
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{2}{constDecl}
 \rail@plus
-\rail@nont{name}
+\rail@nont{name}[]
 \rail@nextplus{1}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{::}
+\rail@term{::}[]
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextbar{1}
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@endbar
 \rail@end
 \rail@begin{6}{mixfix}
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@bar
 \rail@nextbar{2}
-\rail@term{[}
+\rail@term{[}[]
 \rail@plus
-\rail@nont{nat}
+\rail@nont{nat}[]
 \rail@nextplus{3}
-\rail@cterm{,}
+\rail@cterm{,}[]
 \rail@endplus
-\rail@term{]}
+\rail@term{]}[]
 \rail@endbar
-\rail@nont{nat}
+\rail@nont{nat}[]
 \rail@endbar
 \rail@nextbar{4}
-\rail@nont{infix}
+\rail@nont{infix}[]
 \rail@nextbar{5}
-\rail@term{binder}
-\rail@nont{string}
-\rail@nont{nat}
+\rail@term{binder}[]
+\rail@nont{string}[]
+\rail@nont{nat}[]
 \rail@endbar
 \rail@end
 \rail@begin{3}{constdefs}
-\rail@term{constdefs}
+\rail@term{constdefs}[]
 \rail@plus
-\rail@nont{id}
-\rail@term{::}
+\rail@nont{id}[]
+\rail@term{::}[]
 \rail@bar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextbar{1}
-\rail@nont{type}
+\rail@nont{type}[]
 \rail@endbar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@nextplus{2}
 \rail@endplus
 \rail@end
 \rail@begin{4}{trans}
-\rail@term{translations}
+\rail@term{translations}[]
 \rail@plus
-\rail@nont{pat}
+\rail@nont{pat}[]
 \rail@bar
-\rail@term{==}
+\rail@term{==}[]
 \rail@nextbar{1}
-\rail@term{=>}
+\rail@term{=>}[]
 \rail@nextbar{2}
-\rail@term{<=}
+\rail@term{<=}[]
 \rail@endbar
-\rail@nont{pat}
+\rail@nont{pat}[]
 \rail@nextplus{3}
 \rail@endplus
 \rail@end
 \rail@begin{2}{pat}
 \rail@bar
 \rail@nextbar{1}
-\rail@term{(}
-\rail@nont{id}
-\rail@term{)}
+\rail@term{(}[]
+\rail@nont{id}[]
+\rail@term{)}[]
 \rail@endbar
-\rail@nont{string}
+\rail@nont{string}[]
 \rail@end
 \rail@begin{2}{rules}
-\rail@term{rules}
+\rail@term{rules}[]
 \rail@plus
-\rail@nont{id}
-\rail@nont{string}
+\rail@nont{id}[]
+\rail@nont{string}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
 \rail@begin{2}{defs}
-\rail@term{defs}
+\rail@term{defs}[]
 \rail@plus
-\rail@nont{id}
-\rail@nont{string}
+\rail@nont{id}[]
+\rail@nont{string}[]
 \rail@nextplus{1}
 \rail@endplus
 \rail@end
 \rail@begin{1}{oracle}
-\rail@term{oracle}
-\rail@nont{name}
+\rail@term{oracle}[]
+\rail@nont{name}[]
 \rail@end
 \rail@begin{1}{ml}
-\rail@term{ML}
-\rail@nont{text}
+\rail@term{ML}[]
+\rail@nont{text}[]
 \rail@end
 }