*** 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev