Re: [isabelle] Declaring global attributes



On Sat, 22 Oct 2011, John Munroe wrote:

I can't seem to find Attrib.setup_config_int in Isabelle2011.

It is there in the current official release, which is Isabelle2011-1.


Assuming it's the same as Attrib.config_int, the following still gives me an error:

ML {*
val foo = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
*}

declare [[foo = 3]]

The ML foo above is a pair (config, setup). The setup component needs to be applied to the theory context using the 'setup' command in Isar.


	Makarius





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