doc-src/ZF/logics-ZF.rao
author wenzelm
Tue, 04 May 1999 17:59:55 +0200
changeset 6579 d0c6bb2577b1
parent 6156 0d52e7cbff29
permissions -rw-r--r--
isabelle_zf image;

% This file was generated by 'rail' from 'logics-ZF.rai'
\rail@i {1}{ datatype : ( 'datatype' | 'codatatype' ) datadecls; \par datadecls: ( '"' id arglist '"' '=' (constructor + '|') ) + 'and' ; constructor : name ( () | consargs ) ( () | ( '(' mixfix ')' ) ) ; consargs : '(' ('"' var ':' term '"' + ',') ')' ; }
\rail@o {1}{
\rail@begin{2}{datatype}
\rail@bar
\rail@term{datatype}[]
\rail@nextbar{1}
\rail@term{codatatype}[]
\rail@endbar
\rail@nont{datadecls}[]
\rail@end
\rail@begin{3}{datadecls}
\rail@plus
\rail@term{"}[]
\rail@nont{id}[]
\rail@nont{arglist}[]
\rail@term{"}[]
\rail@term{=}[]
\rail@plus
\rail@nont{constructor}[]
\rail@nextplus{1}
\rail@cterm{|}[]
\rail@endplus
\rail@nextplus{2}
\rail@cterm{and}[]
\rail@endplus
\rail@end
\rail@begin{2}{constructor}
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{consargs}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{mixfix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{2}{consargs}
\rail@term{(}[]
\rail@plus
\rail@term{"}[]
\rail@nont{var}[]
\rail@term{:}[]
\rail@nont{term}[]
\rail@term{"}[]
\rail@nextplus{1}
\rail@cterm{,}[]
\rail@endplus
\rail@term{)}[]
\rail@end
}