more NEWS;
authorwenzelm
Fri Aug 18 22:55:24 2017 +0200 (21 months ago)
changeset 664541a73ad1c06dd
parent 66453 cc19f7ca2ed6
child 66455 158c513a39f5
more NEWS;
NEWS
     1.1 --- a/NEWS	Fri Aug 18 20:47:47 2017 +0200
     1.2 +++ b/NEWS	Fri Aug 18 22:55:24 2017 +0200
     1.3 @@ -23,14 +23,22 @@
     1.4  modules around a Language Server implementation.
     1.5  
     1.6  * Theory names are qualified by the session name that they belong to.
     1.7 -This affects imports, but not the theory name space prefix: it remains
     1.8 -the theory base name as before. In order to import theories from other
     1.9 -sessions, the ROOT file format provides a new 'sessions' keyword. In
    1.10 -contrast, a theory that is imported in the old-fashioned manner via an
    1.11 -explicit file-system path belongs to the current session.
    1.12 -
    1.13 -Theories that are imported from other sessions are excluded from the
    1.14 -current session document.
    1.15 +This affects imports, but not the theory name space prefix (which is
    1.16 +just the theory base name as before).
    1.17 +
    1.18 +In order to import theories from other sessions, the ROOT file format
    1.19 +provides a new 'sessions' keyword. In contrast, a theory that is
    1.20 +imported in the old-fashioned manner via an explicit file-system path
    1.21 +belongs to the current session, and might cause theory name confusion
    1.22 +later on. Theories that are imported from other sessions are excluded
    1.23 +from the current session document. The command-line tool "isabelle
    1.24 +imports" helps to update theory imports.
    1.25 +
    1.26 +Properly qualified imports allow the Prover IDE to process arbitrary
    1.27 +theory hierarchies independently of the underlying logic session image
    1.28 +(e.g. option "isabelle jedit -l"), but the directory structure needs to
    1.29 +be known in advance (e.g. option "isabelle jedit -d" or a line in the
    1.30 +file $ISABELLE_HOME_USER/ROOTS).
    1.31  
    1.32  * The main theory entry points for some non-HOL sessions have changed,
    1.33  to avoid confusion with the global name "Main" of the session HOL. This