src/Doc/IsarRef/Inner_Syntax.thy
changeset 56186 01fb1b35433b
parent 55112 b1a5d603fd12
child 56281 03c3d1a7c3b8
equal deleted inserted replaced
56185:851c7b05eb92 56186:01fb1b35433b
  1451     @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1451     @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1452     @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1452     @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1453     @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1453     @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1454     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1454     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1455     @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1455     @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
  1456     @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
  1456     @{ML_antiquotation_def "class_syntax"} & : & @{text "ML antiquotation"} \\
  1457     @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
  1457     @{ML_antiquotation_def "type_syntax"} & : & @{text "ML antiquotation"} \\
  1458     @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
  1458     @{ML_antiquotation_def "const_syntax"} & : & @{text "ML antiquotation"} \\
  1459     @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
  1459     @{ML_antiquotation_def "syntax_const"} & : & @{text "ML antiquotation"} \\
  1460   \end{matharray}
  1460   \end{matharray}
  1461 
  1461 
  1462   Syntax translation functions written in ML admit almost arbitrary
  1462   Syntax translation functions written in ML admit almost arbitrary
  1463   manipulations of inner syntax, at the expense of some complexity and
  1463   manipulations of inner syntax, at the expense of some complexity and
  1464   obscurity in the implementation.
  1464   obscurity in the implementation.