[isabelle-dev] NEWS

[Clemens Ballarin]

* Dropped locale element "includes".  This is a major INCOMPATIBILITY.

In existing theorem specifications replace the includes element by the
respective context elements of the included locale, omitting those that
are already present in the theorem specification.  Multiple assume
elements of a locale should be replaced by a single one involving the
locale predicate.  In the proof body, declarations (most notably
theorems) may be regained by interpreting the respective locales in the
proof context as required (command "interpret").

If using "includes" in replacement of a target solely because the
parameter types in the theorem are not as general as in the target,
consider declaring a new locale with additional type constraints on the
parameters (context element "constrains").

Clemens