* Pure: get_thm interface expects datatype thmref;
* More efficient treatment of intermediate theory checkpoints;

--- 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.