ML antiquotation for simproc_setup
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.
- Projects
- Subscribers
- None