Re: [isabelle] adding "simp" attribute to programmatically created definitions
On Mon, 6 Nov 2006, Michael Norrish wrote:
> name [simp]: "foo == bar"
> 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?
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and