[isabelle-dev] NEWS

Makarius makarius at sketis.net
Sat Mar 29 19:23:59 CET 2008

* Eliminated destructive theorem database.  Potential INCOMPATIBILITY,
really need to observe linear functional update of theories.

* Commands 'use' and 'ML' are now purely functional, operating on
theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.

More information about the isabelle-dev mailing list