NEWS
changeset 65451 5febea96902f
parent 65448 9bc3b57c1fa7
child 65465 067210a08a22
     1.1 --- a/NEWS	Sun Apr 09 20:53:55 2017 +0200
     1.2 +++ b/NEWS	Sun Apr 09 21:06:19 2017 +0200
     1.3 @@ -9,6 +9,18 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* The main theory entry points for some non-HOL sessions have changed,
     1.8 +to avoid confusion with the global name "Main" of the session HOL. This
     1.9 +leads to the follow renamings:
    1.10 +
    1.11 +  CTT/Main.thy    ~>  CTT/CTT.thy
    1.12 +  ZF/Main.thy     ~>  ZF/ZF.thy
    1.13 +  ZF/Main_ZF.thy  ~>  ZF/ZF.thy
    1.14 +  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
    1.15 +  ZF/ZF.thy       ~>  ZF/ZF_Base.thy
    1.16 +
    1.17 +INCOMPATIBILITY.
    1.18 +
    1.19  * Document antiquotations @{prf} and @{full_prf} output proof terms
    1.20  (again) in the same way as commands 'prf' and 'full_prf'.
    1.21