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

Makarius 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 mailing list