Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Greg Bronevetsky wrote:
Addsimps modifies the simpset associated with the current theory,
and Simp_tac uses it (as does simpset ()).
First point: Is the above really what you want, or rather
ALLGOALS (simp_tac (simpset () addsimps [Let_def])) ?
Second point:
In translating Isabelle proofs into Isar I've found that things
depending on the notion of the current theory are liable to misbehave
(including what I've written above).
In Isar I would have to write (in place of my version above),
SIMPSET (fn ss => ALLGOALS (simp_tac (ss addsimps [Let_def]))).
See 10.2.3 of the reference manual.
However I have found in Isar that
ML {*
Addsimps [xxx] ;
*}
seems to work as expected.
Regards,
Jeremy
Last updated: May 03 2024 at 04:19 UTC