Re: [isabelle] referring to constants that have just been defined
Florian Haftmann writes:
> Hello Michael,
> > It seems that using
> > Sign.intern_const
> > will give me the correct qualified name for the constant (I do know
> > its name after all), but I'm worried about the situation when multiple
> > constants from different theories have the same name. What will
> > intern_const do then?
> > Is there a function that will give me the name of the current theory,
> > so that I can construct the fully-qualified name myself?
> Context.theory_name or Sign.full_name may prove helpful. But be aware
> that though the default naming policy is indeed "theory name +
> unqualified name", this might be changed.
Thanks for that. So it does seem as if I should use
In particular, what does intern_const do when there are multiple
constants of the same name in different theories?
This archive was generated by a fusion of
Pipermail (Mailman edition) and