Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Fully qualified access to True and False

view this post on Zulip Email Gateway (Aug 17 2022 at 14:46):

From: Nicole Rauch <rauch@informatik.uni-kl.de>
Hello all,

while it is possible to access most consts via the fully qualified
access Theoryname.constname, this is not possible for (at least) True
and False as defined in HOL.thy. (I.e. if I write HOL.True I get "No
such constant: HOL.True".)
Is there a reason for this strange exception?

Thanks in advance,

Nicole

view this post on Zulip Email Gateway (Aug 17 2022 at 14:46):

From: nipkow@in.tum.de

HOL.True

At the time when Markus introduced qualified names, we decided that the most
frequently used names would not become qualified (for backward compatibility
with existig ML code). This is why HOL.thy has the directive "gobal" right at
the beginning.

Tobias

Last updated: May 03 2024 at 08:18 UTC