1.1 --- a/doc-src/Ref/ref.rao	Thu Jan 08 19:04:33 1998 +0100
     1.2 +++ b/doc-src/Ref/ref.rao	Fri Jan 09 13:49:20 1998 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  % This file was generated by 'rail' from 'ref.rai'
     1.5  \rail@t {lbrace}
     1.6  \rail@t {rbrace}
     1.7 -\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) 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 arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par ml : 'ML' text ; \par }
     1.8 +\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle | local | global ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) 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 arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (name '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par local : 'local' ; \par global : 'global' ; \par ml : 'ML' text ; \par }
     1.9  \rail@o {1}{
    1.10  \rail@begin{2}{theoryDef}
    1.11  \rail@nont{id}[]
    1.12 @@ -35,7 +35,7 @@
    1.13  \rail@nont{ml}[]
    1.14  \rail@endbar
    1.15  \rail@end
    1.16 -\rail@begin{13}{section}
    1.17 +\rail@begin{15}{section}
    1.18  \rail@bar
    1.19  \rail@nont{classes}[]
    1.20  \rail@nextbar{1}
    1.21 @@ -62,6 +62,10 @@
    1.22  \rail@nont{instance}[]
    1.23  \rail@nextbar{12}
    1.24  \rail@nont{oracle}[]
    1.25 +\rail@nextbar{13}
    1.26 +\rail@nont{local}[]
    1.27 +\rail@nextbar{14}
    1.28 +\rail@nont{global}[]
    1.29  \rail@endbar
    1.30  \rail@end
    1.31  \rail@begin{2}{classes}
    1.32 @@ -345,7 +349,7 @@
    1.33  \rail@begin{3}{constdefs}
    1.34  \rail@term{constdefs}[]
    1.35  \rail@plus
    1.36 -\rail@nont{id}[]
    1.37 +\rail@nont{name}[]
    1.38  \rail@term{::}[]
    1.39  \rail@bar
    1.40  \rail@nont{string}[]
    1.41 @@ -407,6 +411,12 @@
    1.42  \rail@term{=}[]
    1.43  \rail@nont{name}[]
    1.44  \rail@end
    1.45 +\rail@begin{1}{local}
    1.46 +\rail@term{local}[]
    1.47 +\rail@end
    1.48 +\rail@begin{1}{global}
    1.49 +\rail@term{global}[]
    1.50 +\rail@end
    1.51  \rail@begin{1}{ml}
    1.52  \rail@term{ML}[]
    1.53  \rail@nont{text}[]