--- a/NEWS Mon Jun 20 22:14:20 2005 +0200
+++ b/NEWS Mon Jun 20 22:14:21 2005 +0200
@@ -161,6 +161,9 @@
* New syntax 'name(i-j, i-, i, ...)' for referring to specific
selections of theorems in named facts via index ranges.
+* More efficient treatment of intermediate checkpoints in interactive
+theory development.
+
*** Locales ***
@@ -459,6 +462,10 @@
Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions
internalize their arguments! INCOMPATIBILITY.
+* Pure: get_thm interface (of PureThy and ProofContext) expects
+datatype thmref (with constructors Name and NameSelection) instead of
+plain string -- INCOMPATIBILITY;
+
* Pure: cases produced by proof methods specify options, where NONE
means to remove case bindings -- INCOMPATIBILITY in
(RAW_)METHOD_CASES.