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 ...
See also section 2.2.4 of the Isabelle/Isar implementation manual.
This archive was generated by a fusion of
Pipermail (Mailman edition) and