doc-src/IsarImplementation/Thy/Syntax.thy
changeset 42510 b9c106763325
parent 39876 1ff9bce085bd
child 45258 97f8806c3ed6
equal deleted inserted replaced
42509:9d107a52b634 42510:b9c106763325
    79   @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
    79   @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
    80   @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
    80   @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
    81   @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
    81   @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
    82   \end{matharray}
    82   \end{matharray}
    83 
    83 
    84   \begin{rail}
    84   @{rail "
    85   ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name
    85   (@@{ML_antiquotation class_syntax} |
    86   ;
    86    @@{ML_antiquotation type_syntax} |
    87   \end{rail}
    87    @@{ML_antiquotation const_syntax} |
       
    88    @@{ML_antiquotation syntax_const}) name
       
    89   "}
    88 
    90 
    89   \begin{description}
    91   \begin{description}
    90 
    92 
    91   \item FIXME
    93   \item FIXME
    92 
    94