Re: [isabelle] defining a constant with a long-identifier name



On Wed, 14 Feb 2007, Michael Norrish wrote:

> I want to (programmatically) define constants that live within
> different sub-spaces of the same theory

> So, how does the record package do it?

A quick search through record_package.ML reveals something like this:

    ...
    |> Theory.add_path bname
    |> Theory.add_consts_i ...
    |> Theory.parent_path

See also section 2.2.4 of the Isabelle/Isar implementation manual.


	Makarius







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