Re: [isabelle] Dependencies on constants



> Also, a simpler issue: for some reason I can't figure out the rules
> about fully-qualified names of constants in theorems. E.g. if I make a
> definition "zulu" in theory Deps, @{const zulu} comes back as:
>   Const ("Dependencies.zulu", "nat \<Rightarrow> bool") : term
> but if I ask about "False" it comes back with:
>   Const ("False", "bool") : term
> What's more, HOL.False does not exist as a constant.
> I'm confused about the rules for when I can count on a fully-qualified
> name and when not. Can you offer any advice?

This one is easy: for historical reasons certain basic constants are
unqualified. If you look into HOL.thy you'll find the keywords "global"
and "local" that control the naming. It is not advisable to use them
yourself.

Tobias





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