doc-src/HOL/logics-HOL.rao

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/HOL/logics-HOL.rao	Sun May 01 17:55:29 2011 +0200
@@ -0,0 +1,210 @@
+% This file was generated by 'rail' from 'logics-HOL.rai'
+\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; \par
+type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
+\rail@o {1}{
+\rail@begin{2}{typedef}
+\rail@term{typedef}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{name}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@nont{type}[]
+\rail@term{=}[]
+\rail@nont{set}[]
+\rail@nont{witness}[]
+\rail@end
+\rail@begin{2}{type}
+\rail@nont{typevarlist}[]
+\rail@nont{name}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{infix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{set}
+\rail@nont{string}[]
+\rail@end
+\rail@begin{2}{witness}
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{id}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+}
+\rail@i {2}{ datatype : 'datatype' typedecls; \par
+typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
+\rail@o {2}{
+\rail@begin{1}{datatype}
+\rail@term{datatype}[]
+\rail@nont{typedecls}[]
+\rail@end
+\rail@begin{3}{typedecls}
+\rail@plus
+\rail@nont{newtype}[]
+\rail@term{=}[]
+\rail@plus
+\rail@nont{cons}[]
+\rail@nextplus{1}
+\rail@cterm{|}[]
+\rail@endplus
+\rail@nextplus{2}
+\rail@cterm{and}[]
+\rail@endplus
+\rail@end
+\rail@begin{2}{newtype}
+\rail@nont{typevarlist}[]
+\rail@nont{id}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{infix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{cons}
+\rail@nont{name}[]
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{argtype}[]
+\rail@endplus
+\rail@bar
+\rail@nextbar{1}
+\rail@term{(}[]
+\rail@nont{mixfix}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+\rail@begin{3}{argtype}
+\rail@bar
+\rail@nont{id}[]
+\rail@nextbar{1}
+\rail@nont{tid}[]
+\rail@nextbar{2}
+\rail@term{(}[]
+\rail@nont{typevarlist}[]
+\rail@nont{id}[]
+\rail@term{)}[]
+\rail@endbar
+\rail@end
+}
+\rail@t {verblbrace}
+\rail@t {verbrbrace}
+\rail@i {3}{ codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); \par
+modespec : '(' ( name * ) ')'; }
+\rail@o {3}{
+\rail@begin{11}{codegen}
+\rail@bar
+\rail@term{code_module}[]
+\rail@nextbar{1}
+\rail@term{code_library}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{modespec}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{name}[]
+\rail@endbar
+\rail@cr{3}
+\rail@bar
+\rail@nextbar{4}
+\rail@term{file}[]
+\rail@nont{name}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{4}
+\rail@term{imports}[]
+\rail@plus
+\rail@nont{name}[]
+\rail@nextplus{5}
+\rail@endplus
+\rail@endbar
+\rail@cr{7}
+\rail@term{contains}[]
+\rail@bar
+\rail@plus
+\rail@nont{name}[]
+\rail@term{=}[]
+\rail@nont{term}[]
+\rail@nextplus{8}
+\rail@endplus
+\rail@nextbar{9}
+\rail@plus
+\rail@nont{term}[]
+\rail@nextplus{10}
+\rail@endplus
+\rail@endbar
+\rail@end
+\rail@begin{2}{modespec}
+\rail@term{(}[]
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{name}[]
+\rail@endplus
+\rail@term{)}[]
+\rail@end
+}
+\rail@i {4}{ constscode : 'consts_code' (codespec +); \par
+codespec : const template attachment ?; \par
+typescode : 'types_code' (tycodespec +); \par
+tycodespec : name template attachment ?; \par
+const : term; \par
+template: '(' string ')'; \par
+attachment: 'attach' modespec ? verblbrace text verbrbrace; }
+\rail@o {4}{
+\rail@begin{2}{constscode}
+\rail@term{consts_code}[]
+\rail@plus
+\rail@nont{codespec}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{codespec}
+\rail@nont{const}[]
+\rail@nont{template}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{attachment}[]
+\rail@endbar
+\rail@end
+\rail@begin{2}{typescode}
+\rail@term{types_code}[]
+\rail@plus
+\rail@nont{tycodespec}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\rail@begin{2}{tycodespec}
+\rail@nont{name}[]
+\rail@nont{template}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{attachment}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{const}
+\rail@nont{term}[]
+\rail@end
+\rail@begin{1}{template}
+\rail@term{(}[]
+\rail@nont{string}[]
+\rail@term{)}[]
+\rail@end
+\rail@begin{2}{attachment}
+\rail@term{attach}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{modespec}[]
+\rail@endbar
+\rail@token{verblbrace}[]
+\rail@nont{text}[]
+\rail@token{verbrbrace}[]
+\rail@end
+}