* improved thms_containing: proper indexing of facts instead of raw
authorwenzelm
Tue, 02 Jul 2002 15:54:21 +0200
changeset 13280 306ef3aef61b
parent 13279 8a722689a1c9
child 13281 5e89b6a4ec15
* improved thms_containing: proper indexing of facts instead of raw theorems; check validity of results wrt. current name space; include local facts of proof configuration (also covers active locales);
NEWS
--- a/NEWS	Tue Jul 02 15:45:55 2002 +0200
+++ b/NEWS	Tue Jul 02 15:54:21 2002 +0200
@@ -1,6 +1,17 @@
+
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+New in this Isabelle release
+----------------------------
+
+*** General ***
+
+* improved thms_containing: proper indexing of facts instead of raw
+theorems; check validity of results wrt. current name space; include
+local facts of proof configuration (also covers active locales);
+
+
 *** HOL ***
 
 * arith(_tac) does now know about div k and mod k where k is a numeral of
@@ -10,6 +21,8 @@
 * simp's arithmetic capabilities have been enhanced a bit:
   it now takes ~= in premises into account (by performing a case split).
 
+
+
 New in Isabelle2002 (March 2002)
 --------------------------------