1.1 --- a/NEWS	Wed May 12 12:51:32 2010 +0200
     1.2 +++ b/NEWS	Wed May 12 13:21:23 2010 +0200
     1.3 @@ -3317,7 +3317,7 @@
     1.4  * Pure: axiomatic type classes are now purely definitional, with
     1.5  explicit proofs of class axioms and super class relations performed
     1.6  internally. See Pure/axclass.ML for the main internal interfaces --
     1.7 -notably AxClass.define_class supersedes AxClass.add_axclass, and
     1.8 +notably AxClass.define_class supercedes AxClass.add_axclass, and
     1.9  AxClass.axiomatize_class/classrel/arity supersede
    1.10  Sign.add_classes/classrel/arities.
    1.11  
    1.12 @@ -4211,7 +4211,7 @@
    1.13  * Pure/library.ML: the exception LIST has been given up in favour of
    1.14  the standard exceptions Empty and Subscript, as well as
    1.15  Library.UnequalLengths.  Function like Library.hd and Library.tl are
    1.16 -superseded by the standard hd and tl functions etc.
    1.17 +superceded by the standard hd and tl functions etc.
    1.18  
    1.19  A number of basic list functions are no longer exported to the ML
    1.20  toplevel, as they are variants of predefined functions.  The following
    1.21 @@ -4342,15 +4342,15 @@
    1.22  
    1.23  * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
    1.24  fold_types traverse types/terms from left to right, observing natural
    1.25 -argument order.  Supersedes previous foldl_XXX versions, add_frees,
    1.26 +argument order.  Supercedes previous foldl_XXX versions, add_frees,
    1.27  add_vars etc. have been adapted as well: INCOMPATIBILITY.
    1.28  
    1.29  * Pure: name spaces have been refined, with significant changes of the
    1.30  internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
    1.31 -to extern(_table).  The plain name entry path is superseded by a
    1.32 +to extern(_table).  The plain name entry path is superceded by a
    1.33  general 'naming' context, which also includes the 'policy' to produce
    1.34  a fully qualified name and external accesses of a fully qualified
    1.35 -name; NameSpace.extend is superseded by context dependent
    1.36 +name; NameSpace.extend is superceded by context dependent
    1.37  Sign.declare_name.  Several theory and proof context operations modify
    1.38  the naming context.  Especially note Theory.restore_naming and
    1.39  ProofContext.restore_naming to get back to a sane state; note that
    1.40 @@ -4390,7 +4390,7 @@
    1.41  etc.) as well as the sign field in Thm.rep_thm etc. have been retained
    1.42  for convenience -- they merely return the theory.
    1.43  
    1.44 -* Pure: type Type.tsig is superseded by theory in most interfaces.
    1.45 +* Pure: type Type.tsig is superceded by theory in most interfaces.
    1.46  
    1.47  * Pure: the Isar proof context type is already defined early in Pure
    1.48  as Context.proof (note that ProofContext.context and Proof.context are
    1.49 @@ -5522,7 +5522,7 @@
    1.50    Eps_sym_eq       -> some_sym_eq_trivial
    1.51    Eps_eq           -> some_eq_trivial
    1.52  
    1.53 -* HOL: exhaust_tac on datatypes superseded by new generic case_tac;
    1.54 +* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
    1.55  
    1.56  * HOL: removed obsolete theorem binding expand_if (refer to split_if
    1.57  instead);
    1.58 @@ -5660,7 +5660,7 @@
    1.59  replaced "delrule" by "rule del";
    1.60  
    1.61  * Isar/Provers: new 'hypsubst' method, plain 'subst' method and
    1.62 -'symmetric' attribute (the latter supersedes [RS sym]);
    1.63 +'symmetric' attribute (the latter supercedes [RS sym]);
    1.64  
    1.65  * Isar/Provers: splitter support (via 'split' attribute and 'simp'
    1.66  method modifier); 'simp' method: 'only:' modifier removes loopers as