[isabelle-dev] NEWS: session-qualified theory names are mandatory

Makarius makarius at sketis.net
Fri Sep 29 23:06:46 CEST 2017


*** General ***

* Session-qualified theory names are mandatory: it is no longer possible
to refer to unqualified theories from the parent session.
INCOMPATIBILITY for old developments that have not been updated to
Isabelle2017 yet (using the "isabelle imports" tool).


This refers to Isabelle/4c98c929a12a. It means that after the
Isabelle2017 everything becomes really serious about qualified theory
names, e.g. session images no longer affect the theory name space.

It will eventually have further impact on isabelle build.


	Makarius


More information about the isabelle-dev mailing list