ML

• ML antiquotation simproc_setup inlines an invocation of Simplifier.simproc_setup, using the same concrete syntax as the corresponding Isar command. This allows to introduce a new simproc conveniently within an ML module, and refer directly to its ML value. For example, the simproc Record.eq is defined in ~~/src/HOL/Tools/record.ML as follows:

val eq_simproc = \<^simproc_setup>‹eq ("r = s") = ‹K eq_proc››;

• Simplification procedures may be distinguished via characteristic theorems that are specified as identifier in ML antiquotation simproc_setup (but not in the corresponding Isar command). This allows to work with several versions of the simproc, e.g. due to locale interpretations.

This refers to Isabelle/9d44cc361f19.