tuned;
authorwenzelm
Mon Mar 17 20:54:41 2014 +0100 (2014-03-17)
changeset 5618601fb1b35433b
parent 56185 851c7b05eb92
child 56187 2666cd7d380c
tuned;
src/Doc/IsarRef/Inner_Syntax.thy
     1.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Mon Mar 17 20:48:58 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Mon Mar 17 20:54:41 2014 +0100
     1.3 @@ -1453,10 +1453,10 @@
     1.4      @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     1.5      @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     1.6      @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     1.7 -    @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
     1.8 -    @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
     1.9 -    @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
    1.10 -    @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
    1.11 +    @{ML_antiquotation_def "class_syntax"} & : & @{text "ML antiquotation"} \\
    1.12 +    @{ML_antiquotation_def "type_syntax"} & : & @{text "ML antiquotation"} \\
    1.13 +    @{ML_antiquotation_def "const_syntax"} & : & @{text "ML antiquotation"} \\
    1.14 +    @{ML_antiquotation_def "syntax_const"} & : & @{text "ML antiquotation"} \\
    1.15    \end{matharray}
    1.16  
    1.17    Syntax translation functions written in ML admit almost arbitrary