[isabelle-dev] NEWS: old 'def' command has been discontinued
makarius at sketis.net
Mon Dec 4 16:11:44 CET 2017
*** 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.
More information about the isabelle-dev