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



> 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





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