--- a/NEWS Wed May 12 11:07:46 2010 +0200
+++ b/NEWS Wed May 12 11:08:15 2010 +0200
@@ -143,7 +143,11 @@
* 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.
@@ -160,9 +164,12 @@
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.
@@ -322,6 +329,58 @@
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
@@ -3257,7 +3316,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 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.
@@ -4151,7 +4210,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
-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
@@ -4282,15 +4341,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. 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
@@ -4330,7 +4389,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 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
@@ -5462,7 +5521,7 @@
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);
@@ -5600,7 +5659,7 @@
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