Re: [isabelle] Attribute code called 3 times

Hi Cezary,

This effect is due to the Haftmann and Wenzel "local theory sandwich".
It's once called for the auxillary context, once for the local context, and once for the theory context.

It somewhat stores the data in three different layers.
However, when you lookup data, you will probably only see one version from the one layer you are working in.

What's the point of getting it called only once anyway?


On 03/10/2012 11:38 PM, Cezary Kaliszyk wrote:
Hi all,

I want to define an attribute, that takes a string as an argument
with the code below:

ML {* fun attr s = let val _ = warning s in
       (Thm.rule_attribute (fn _ =>  fn y =>  y)) end *}
setup {* Attrib.setup ( "map_const")
       (Scan.lift Parse.string>>  attr) "..." *}
lemma [map_const "foo"]: True
   by simp

However upon defining the lemma, "foo" is printed 3 times. Is there a
good reason why the attribute code is called 3 times and is it
possible to get it called only once?



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