NEWS

 *** HOL ***
 
 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
 no longer shadowed.  INCOMPATIBILITY.
 
-* Dropped theorem duplicate comp_arith; use semiring_norm instead.  INCOMPATIBILITY.
+* Dropped theorem duplicate comp_arith; use semiring_norm instead.
+INCOMPATIBILITY.
+
+* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
+INCOMPATIBILITY.
 
 * Dropped normalizing. Use semiring classes directly. INCOMPATIBILITY.
 
 * Theory 'Finite_Set': various folding_* locales facilitate the application
 of the various fold combinators on finite sets.

 introducing dependencies on parameters or assumptions, which is not
 possible in Isabelle/Pure/HOL.  Note that the logical environment may
 contain multiple interpretations of local typedefs (with different
 non-emptiness proofs), even in a global theory context.
 
-* Theory Library/Coinductive_List has been removed -- superceded by
+* Theory Library/Coinductive_List has been removed -- superseded by
 AFP/thys/Coinductive.
+
+* Theory PReal, including the type "preal" and related operations, has
+been removed.  INCOMPATIBILITY.
 
 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
 Min, Max from theory Finite_Set.  INCOMPATIBILITY.
 
 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.

   Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
   Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
   Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
   Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
+
+
+*** HOLCF ***
+
+* Variable names in lemmas generated by the domain package have
+changed; the naming scheme is now consistent with the HOL datatype
+package.  Some proof scripts may be affected, INCOMPATIBILITY.
+
+* The domain package no longer defines the function "foo_copy" for
+recursive domain "foo".  The reach lemma is now stated directly in
+terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
+be reformulated in terms of "foo_take", INCOMPATIBILITY.
+
+* Most definedness lemmas generated by the domain package (previously
+of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
+like "foo$x = UU <-> x = UU", which works better as a simp rule.
+Proof scripts that used definedness lemmas as intro rules may break,
+potential INCOMPATIBILITY.
+
+* Induction and casedist rules generated by the domain package now
+declare proper case_names (one called "bottom", and one named for each
+constructor).  INCOMPATIBILITY.
+
+* For mutually-recursive domains, separate "reach" and "take_lemma"
+rules are generated for each domain, INCOMPATIBILITY.
+
+  foo_bar.reach       ~> foo.reach  bar.reach
+  foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
+
+* Some lemmas generated by the domain package have been renamed for
+consistency with the datatype package, INCOMPATIBILITY.
+
+  foo.ind        ~> foo.induct
+  foo.finite_ind ~> foo.finite_induct
+  foo.coind      ~> foo.coinduct
+  foo.casedist   ~> foo.exhaust
+  foo.exhaust    ~> foo.nchotomy
+
+* For consistency with other definition packages, the fixrec package
+now generates qualified theorem names, INCOMPATIBILITY.
+
+  foo_simps  ~> foo.simps
+  foo_unfold ~> foo.unfold
+  foo_induct ~> foo.induct
+
+* The "contlub" predicate has been removed.  Proof scripts should use
+lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
+
+* The "admw" predicate has been removed, INCOMPATIBILITY.
+
+* The constants cpair, cfst, and csnd have been removed in favor of
+Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
 
 
 *** ML ***
 
 * Sorts.certify_sort and derived "cert" operations for types and terms

 potential INCOMPATIBILITY.
 
 * 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 supercedes AxClass.add_axclass, and
+notably AxClass.define_class supersedes AxClass.add_axclass, and
 AxClass.axiomatize_class/classrel/arity supersede
 Sign.add_classes/classrel/arities.
 
 * Pure/Isar: Args/Attrib parsers operate on Context.generic --
 global/local versions on theory vs. Proof.context have been

 accordingly, while Option.map replaces apsome.
 
 * 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
-superceded by the standard hd and tl functions etc.
+superseded 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
 suggests how one can translate existing code:
 

 particular order for Symtab.keys, Symtab.dest, etc. (consider using
 Library.sort_strings on result).
 
 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
 fold_types traverse types/terms from left to right, observing natural
-argument order.  Supercedes previous foldl_XXX versions, add_frees,
+argument order.  Supersedes 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 superceded by a
+to extern(_table).  The plain name entry path is superseded 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 superceded by context dependent
+name; NameSpace.extend is superseded 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
 Theory.add_path is no longer sufficient to recover from
 Theory.absolute_path in particular.

 
 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm
 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 superceded by theory in most interfaces.
+* Pure: type Type.tsig is superseded 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
 aliases, where the latter is the preferred name).  This enables other
 Isabelle components to refer to that type even before Isar is present.

   selectI          -> someI
   select1_equality -> some1_equality
   Eps_sym_eq       -> some_sym_eq_trivial
   Eps_eq           -> some_eq_trivial
 
-* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
+* HOL: exhaust_tac on datatypes superseded by new generic case_tac;
 
 * HOL: removed obsolete theorem binding expand_if (refer to split_if
 instead);
 
 * HOL: the recursion equations generated by 'recdef' are now called

 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
 most cases, one should have to change intro!! to intro? only);
 replaced "delrule" by "rule del";
 
 * Isar/Provers: new 'hypsubst' method, plain 'subst' method and
-'symmetric' attribute (the latter supercedes [RS sym]);
+'symmetric' attribute (the latter supersedes [RS sym]);
 
 * Isar/Provers: splitter support (via 'split' attribute and 'simp'
 method modifier); 'simp' method: 'only:' modifier removes loopers as
 well (including splits);