[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