% 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 }
\rail@o {1}{
\rail@begin{2}{theoryDef}
\rail@nont{id}
\rail@term{=}
\rail@plus
\rail@nont{name}
\rail@nextplus{1}
\rail@cterm{+}
\rail@endplus
\rail@bar
\rail@term{+}
\rail@nont{extension}
\rail@nextbar{1}
\rail@endbar
\rail@end
\rail@begin{2}{name}
\rail@bar
\rail@nont{id}
\rail@nextbar{1}
\rail@nont{string}
\rail@endbar
\rail@end
\rail@begin{2}{extension}
\rail@plus
\rail@nont{section}
\rail@nextplus{1}
\rail@endplus
\rail@term{end}
\rail@bar
\rail@nextbar{1}
\rail@nont{ml}
\rail@endbar
\rail@end
\rail@begin{10}{section}
\rail@bar
\rail@nont{classes}
\rail@nextbar{1}
\rail@nont{default}
\rail@nextbar{2}
\rail@nont{types}
\rail@nextbar{3}
\rail@nont{arities}
\rail@nextbar{4}
\rail@nont{consts}
\rail@nextbar{5}
\rail@nont{constdefs}
\rail@nextbar{6}
\rail@nont{trans}
\rail@nextbar{7}
\rail@nont{defs}
\rail@nextbar{8}
\rail@nont{rules}
\rail@nextbar{9}
\rail@nont{oracle}
\rail@endbar
\rail@end
\rail@begin{4}{classes}
\rail@term{classes}
\rail@plus
\rail@nont{id}
\rail@bar
\rail@nextbar{1}
\rail@term{<}
\rail@plus
\rail@nont{id}
\rail@nextplus{2}
\rail@cterm{,}
\rail@endplus
\rail@endbar
\rail@nextplus{3}
\rail@endplus
\rail@end
\rail@begin{1}{default}
\rail@term{default}
\rail@nont{sort}
\rail@end
\rail@begin{4}{sort}
\rail@bar
\rail@nont{id}
\rail@nextbar{1}
\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "4266308 $}
\rail@bar
\rail@nextbar{2}
\rail@plus
\rail@nont{id}
\rail@nextplus{3}
\rail@cterm{,}
\rail@endplus
\rail@endbar
\rail@term{\protect \relax $\mathsurround =\z@ \delimiter "5267309 $}
\rail@endbar
\rail@end
\rail@begin{3}{types}
\rail@term{types}
\rail@plus
\rail@nont{typeDecl}
\rail@bar
\rail@nextbar{1}
\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@nextbar{1}
\rail@term{infixl}
\rail@endbar
\rail@nont{nat}
\rail@end
\rail@begin{3}{typeDecl}
\rail@nont{typevarlist}
\rail@nont{name}
\rail@bar
\rail@nextbar{1}
\rail@term{=}
\rail@bar
\rail@nont{string}
\rail@nextbar{2}
\rail@nont{type}
\rail@endbar
\rail@endbar
\rail@end
\rail@begin{4}{typevarlist}
\rail@bar
\rail@nextbar{1}
\rail@nont{tid}
\rail@nextbar{2}
\rail@term{(}
\rail@plus
\rail@nont{tid}
\rail@nextplus{3}
\rail@cterm{,}
\rail@endplus
\rail@term{)}
\rail@endbar
\rail@end
\rail@begin{5}{type}
\rail@bar
\rail@nont{simpleType}
\rail@nextbar{1}
\rail@term{(}
\rail@nont{type}
\rail@term{)}
\rail@nextbar{2}
\rail@nont{type}
\rail@term{=>}
\rail@nont{type}
\rail@nextbar{3}
\rail@term{[}
\rail@plus
\rail@nont{type}
\rail@nextplus{4}
\rail@cterm{,}
\rail@endplus
\rail@term{]}
\rail@term{=>}
\rail@nont{type}
\rail@endbar
\rail@end
\rail@begin{6}{simpleType}
\rail@bar
\rail@nont{id}
\rail@nextbar{1}
\rail@nont{tid}
\rail@bar
\rail@nextbar{2}
\rail@term{::}
\rail@nont{id}
\rail@endbar
\rail@nextbar{3}
\rail@term{(}
\rail@plus
\rail@nont{type}
\rail@nextplus{4}
\rail@cterm{,}
\rail@endplus
\rail@term{)}
\rail@nont{id}
\rail@nextbar{5}
\rail@nont{simpleType}
\rail@nont{id}
\rail@endbar
\rail@end
\rail@begin{3}{arities}
\rail@term{arities}
\rail@plus
\rail@plus
\rail@nont{name}
\rail@nextplus{1}
\rail@cterm{,}
\rail@endplus
\rail@term{::}
\rail@nont{arity}
\rail@nextplus{2}
\rail@endplus
\rail@end
\rail@begin{3}{arity}
\rail@bar
\rail@nextbar{1}
\rail@term{(}
\rail@plus
\rail@nont{sort}
\rail@nextplus{2}
\rail@cterm{,}
\rail@endplus
\rail@term{)}
\rail@endbar
\rail@nont{id}
\rail@end
\rail@begin{3}{consts}
\rail@term{consts}
\rail@plus
\rail@nont{constDecl}
\rail@bar
\rail@nextbar{1}
\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@nextplus{1}
\rail@cterm{,}
\rail@endplus
\rail@term{::}
\rail@bar
\rail@nont{string}
\rail@nextbar{1}
\rail@nont{type}
\rail@endbar
\rail@end
\rail@begin{6}{mixfix}
\rail@bar
\rail@nont{string}
\rail@bar
\rail@nextbar{1}
\rail@bar
\rail@nextbar{2}
\rail@term{[}
\rail@plus
\rail@nont{nat}
\rail@nextplus{3}
\rail@cterm{,}
\rail@endplus
\rail@term{]}
\rail@endbar
\rail@nont{nat}
\rail@endbar
\rail@nextbar{4}
\rail@nont{infix}
\rail@nextbar{5}
\rail@term{binder}
\rail@nont{string}
\rail@nont{nat}
\rail@endbar
\rail@end
\rail@begin{3}{constdefs}
\rail@term{constdefs}
\rail@plus
\rail@nont{id}
\rail@term{::}
\rail@bar
\rail@nont{string}
\rail@nextbar{1}
\rail@nont{type}
\rail@endbar
\rail@nont{string}
\rail@nextplus{2}
\rail@endplus
\rail@end
\rail@begin{4}{trans}
\rail@term{translations}
\rail@plus
\rail@nont{pat}
\rail@bar
\rail@term{==}
\rail@nextbar{1}
\rail@term{=>}
\rail@nextbar{2}
\rail@term{<=}
\rail@endbar
\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@endbar
\rail@nont{string}
\rail@end
\rail@begin{2}{rules}
\rail@term{rules}
\rail@plus
\rail@nont{id}
\rail@nont{string}
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{2}{defs}
\rail@term{defs}
\rail@plus
\rail@nont{id}
\rail@nont{string}
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{1}{oracle}
\rail@term{oracle}
\rail@nont{name}
\rail@end
\rail@begin{1}{ml}
\rail@term{ML}
\rail@nont{text}
\rail@end
}