[isabelle-dev] NEWS: old 'def' command has been discontinued

[Makarius]

*** General ***

* The old 'def' command has been discontinued (legacy since
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.


This refers to Isabelle/acb0807ddb56.

This small reform may serve as an example of AFP maintenance. I've spent
many years to have the Prover IDE edit projects as a whole, and we are
now pretty close to that due to the reform of session-qualified theory
names. Full scalability is still somewhat lacking, though: It requires a
bit of thinking and planning which sessions to edit in which order. The
ML process can sometimes become overloaded and spend minutes on GC /
heap compaction. The JVM process is also quite easy to overload with
tons of PIDE markup; maybe there are even memory leaks.


	Makarius