[isabelle-dev] NEWS: main theory entry points
Makarius
makarius at sketis.net
Wed Apr 12 14:47:03 CEST 2017
*** General ***
* The main theory entry points for some non-HOL sessions have changed,
to avoid confusion with the global name "Main" of the session HOL. This
leads to the follow renamings:
CTT/Main.thy ~> CTT/CTT.thy
ZF/Main.thy ~> ZF/ZF.thy
ZF/Main_ZF.thy ~> ZF/ZF.thy
ZF/Main_ZFC.thy ~> ZF/ZFC.thy
ZF/ZF.thy ~> ZF/ZF_Base.thy
INCOMPATIBILITY.
This refers to Isabelle/5febea96902f. It belongs to cleanup and
clarification towards session-qualified theory names, with the exception
of a few important global entry points like "Pure", "Main", "Complex_Main".
Makarius
More information about the isabelle-dev
mailing list