# HG changeset patch
# User wenzelm
# Date 1491764779 -7200
# Node ID 5febea96902fc350b3b096b0eb35b516a07988e8
# Parent  b0a73039ddaab2e78267f42e3451a9a6c37c8998
NEWS;

diff -r b0a73039ddaa -r 5febea96902f NEWS
--- 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'.