* Pure/obtain: "thesis" now internal (use ?thesis);
* Pure: generic 'sym' / 'symmetric' attributes;
* Provers/classical: 'swapped' attribute;
* HOL: proper rules less_induct and wf_induct_rule;

--- a/NEWS	Thu Dec 06 00:43:03 2001 +0100
+++ b/NEWS	Thu Dec 06 00:45:04 2001 +0100
@@ -109,6 +109,14 @@
 * Pure: "sorry" no longer requires quick_and_dirty in interactive
 mode;
 
+* Pure/obtain: the formal conclusion "thesis", being marked as
+``internal'', may no longer be reference directly in the text;
+potential INCOMPATIBILITY, may need to use "?thesis" in rare
+situations;
+
+* Pure: generic 'sym' attribute which declares a rule both as pure
+'elim?' and for the 'symmetric' operation;
+
 * Pure/Provers/classical: simplified integration with pure rule
 attributes and methods; the classical "intro?/elim?/dest?"
 declarations coincide with the pure ones; the "rule" method no longer
@@ -117,6 +125,9 @@
 AddXIs/AddXEs/AddXDs; all of this has some potential for
 INCOMPATIBILITY;
 
+* Provers/classical: attribute 'swapped' produces classical inversions
+of introduction rules;
+
 * Provers/simplifier: 'simplified' attribute may refer to explicit
 rules instead of full simplifier context; 'iff' attribute handles
 conditional rules;
@@ -129,6 +140,9 @@
 * HOL: 'inductive' no longer features separate (collective) attributes
 for 'intros' (was found too confusing);
 
+* HOL: properly declared induction rules less_induct and
+wf_induct_rule;
+
 * HOLCF: domain package adapted to new-style theories, e.g. see
 HOLCF/ex/Dnat.thy;