--- a/NEWS Sun Apr 09 20:53:55 2017 +0200
+++ b/NEWS Sun Apr 09 21:06:19 2017 +0200
@@ -9,6 +9,18 @@
*** 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.
+
* Document antiquotations @{prf} and @{full_prf} output proof terms
(again) in the same way as commands 'prf' and 'full_prf'.