--- a/NEWS Fri Nov 03 21:35:59 2000 +0100
+++ b/NEWS Sat Nov 04 18:39:44 2000 +0100
@@ -8,6 +8,8 @@
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
+* Isar: 'obtain' no longer declares "that" fact as simp/intro;
+
*** Document preparation ***
@@ -24,10 +26,21 @@
into document output unless you really know what you are doing!
-
*** Isar ***
-* HOL: default proof step now includes 'intro_classes';
+* Pure: assumption method (an implicit finishing) now handles actual
+rules as well;
+
+* Pure: improved 'obtain' --- moved to Pure, insert "that" into
+initial goal, declare "that" only as Pure intro (only for single
+steps); the "that" rule assumption may now be involved in implicit
+finishing, thus ".." becomes a feasible for trivial obtains;
+
+* Pure: default proof step now includes 'intro_classes'; thus trivial
+instance proofs may be performed by "..";
+
+* Pure: ?thesis / ?this / "..." now work for pure meta-level
+statements as well;
*** HOL ***
@@ -38,6 +51,16 @@
HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
(as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
+* HOL/typedef: simplified package, provide more useful rules (see also
+HOL/subset.thy);
+
+
+*** General ***
+
+* Provers: fast_tac (and friends) now handle actual object-logic rules
+as assumptions as well;
+
+
New in Isabelle99-1 (October 2000)
----------------------------------