Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/Ref/ref.rao
changeset 2657 448bb82c4003
child 3098 a31170b67367 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/ref.rao	Thu Feb 20 15:13:52 1997 +0100
@@ -0,0 +1,329 @@
+% 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
+}
isabelle