# HG changeset patch
# User wenzelm
# Date 973359584 -3600
# Node ID 0025fd11882ca6694596ad6145547f6b13b981f3
# Parent  1d54567bed24eaa6863dc7d628b7d310c7476274
misc stuff;

diff -r 1d54567bed24 -r 0025fd11882c NEWS
--- 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)
 ----------------------------------