reverted parts of 7902dc7ea11d -- note that NEWS of published Isabelle releases are essentially read-only;
(Spelling note: "supersede" is indeed more common in Isabelle sources, although "supercede" is also correct according to major dictionaries.)

--- a/NEWS	Wed May 12 12:51:32 2010 +0200
+++ b/NEWS	Wed May 12 13:21:23 2010 +0200
@@ -3317,7 +3317,7 @@
 * Pure: axiomatic type classes are now purely definitional, with
 explicit proofs of class axioms and super class relations performed
 internally. See Pure/axclass.ML for the main internal interfaces --
-notably AxClass.define_class supersedes AxClass.add_axclass, and
+notably AxClass.define_class supercedes AxClass.add_axclass, and
 AxClass.axiomatize_class/classrel/arity supersede
 Sign.add_classes/classrel/arities.
 
@@ -4211,7 +4211,7 @@
 * Pure/library.ML: the exception LIST has been given up in favour of
 the standard exceptions Empty and Subscript, as well as
 Library.UnequalLengths.  Function like Library.hd and Library.tl are
-superseded by the standard hd and tl functions etc.
+superceded by the standard hd and tl functions etc.
 
 A number of basic list functions are no longer exported to the ML
 toplevel, as they are variants of predefined functions.  The following
@@ -4342,15 +4342,15 @@
 
 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
 fold_types traverse types/terms from left to right, observing natural
-argument order.  Supersedes previous foldl_XXX versions, add_frees,
+argument order.  Supercedes previous foldl_XXX versions, add_frees,
 add_vars etc. have been adapted as well: INCOMPATIBILITY.
 
 * Pure: name spaces have been refined, with significant changes of the
 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
-to extern(_table).  The plain name entry path is superseded by a
+to extern(_table).  The plain name entry path is superceded by a
 general 'naming' context, which also includes the 'policy' to produce
 a fully qualified name and external accesses of a fully qualified
-name; NameSpace.extend is superseded by context dependent
+name; NameSpace.extend is superceded by context dependent
 Sign.declare_name.  Several theory and proof context operations modify
 the naming context.  Especially note Theory.restore_naming and
 ProofContext.restore_naming to get back to a sane state; note that
@@ -4390,7 +4390,7 @@
 etc.) as well as the sign field in Thm.rep_thm etc. have been retained
 for convenience -- they merely return the theory.
 
-* Pure: type Type.tsig is superseded by theory in most interfaces.
+* Pure: type Type.tsig is superceded by theory in most interfaces.
 
 * Pure: the Isar proof context type is already defined early in Pure
 as Context.proof (note that ProofContext.context and Proof.context are
@@ -5522,7 +5522,7 @@
   Eps_sym_eq       -> some_sym_eq_trivial
   Eps_eq           -> some_eq_trivial
 
-* HOL: exhaust_tac on datatypes superseded by new generic case_tac;
+* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
 
 * HOL: removed obsolete theorem binding expand_if (refer to split_if
 instead);
@@ -5660,7 +5660,7 @@
 replaced "delrule" by "rule del";
 
 * Isar/Provers: new 'hypsubst' method, plain 'subst' method and
-'symmetric' attribute (the latter supersedes [RS sym]);
+'symmetric' attribute (the latter supercedes [RS sym]);
 
 * Isar/Provers: splitter support (via 'split' attribute and 'simp'
 method modifier); 'simp' method: 'only:' modifier removes loopers as