NEWS
changeset 65504 b80477da30eb
parent 65465 067210a08a22
child 65505 741fad555d82
     1.1 --- a/NEWS	Tue Apr 18 14:19:49 2017 +0200
     1.2 +++ b/NEWS	Tue Apr 18 14:51:46 2017 +0200
     1.3 @@ -9,6 +9,13 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Theory names are qualified by the session name that they belong to.
     1.8 +This affects imports, but not the theory name space prefix: it remains
     1.9 +the theory base name as before. In order to import theories from other
    1.10 +sessions, the ROOT file format provides a new 'sessions' keyword. In
    1.11 +contrast, a theory that is imported in the old-fashioned manner via an
    1.12 +explicit file-system path belongs to the current session.
    1.13 +
    1.14  * The main theory entry points for some non-HOL sessions have changed,
    1.15  to avoid confusion with the global name "Main" of the session HOL. This
    1.16  leads to the follow renamings: