Re: [isabelle] adding "simp" attribute to programmatically created definitions



On Mon, 6 Nov 2006, Michael Norrish wrote:

> defs(overloaded)  
>   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).


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.