Email Gateway (Aug 18 2022 at 09:52): Email Gateway (Aug 18 2022 at 09:52):From: Michael Norrish <Michael.Norrish@nicta.com.au>
I'm using PureThy.add_defs_i to define an overloaded constant. I want
the resulting theorem to have the simp attribute, as if someone had
written
defs(overloaded)
name [simp]: "foo == bar"
From reading source code, it looks as if I should call
PureThy.add_defs_i true [((name, tm), [Simplifier.simp_add])]
to get this effect (where tm is the term corresponding to "foo ==
bar"). Is this right?
Thanks,
Michael.
Email Gateway (Aug 18 2022 at 09:52):From: Makarius <makarius@sketis.net>
This is perfectly right concerning Isabelle2005 (and before). For the
near future, we are in the middle of changing all these basic mechanisms
(the old entry points won't disappear, but become irrelevant).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC