--- a/NEWS Mon Aug 04 17:53:17 2014 +0200
+++ b/NEWS Mon Aug 04 17:55:11 2014 +0200
@@ -355,9 +355,9 @@
- a type variable as a raw type is supported
- stronger reflexivity prover
- rep_eq is always generated by lift_definition
- - setup for Lifting/Transfer is now automated for BNFs
+ - setup for Lifting/Transfer is now automated for BNFs
+ holds for BNFs that do not contain a dead variable
- + relator_eq, relator_mono, relator_distr, relator_domain,
+ + relator_eq, relator_mono, relator_distr, relator_domain,
relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
right_unique, right_total, left_unique, left_total are proved
automatically
@@ -365,13 +365,13 @@
+ simplification rules for a predicator definition are proved
automatically for datatypes
- consolidation of the setup of Lifting/Transfer
- + property that a relator preservers reflexivity is not needed any
+ + property that a relator preservers reflexivity is not needed any
more
Minor INCOMPATIBILITY.
- + left_total and left_unique rules are now transfer rules
+ + left_total and left_unique rules are now transfer rules
(reflexivity_rule attribute not needed anymore)
INCOMPATIBILITY.
- + Domainp does not have to be a separate assumption in
+ + Domainp does not have to be a separate assumption in
relator_domain theorems (=> more natural statement)
INCOMPATIBILITY.
- registration of code equations is more robust
@@ -381,12 +381,12 @@
Potential INCOMPATIBILITY.
- eq_onp is always unfolded in respectfulness proof obligation
Potential INCOMPATIBILITY.
- - unregister lifting setup for Code_Numeral.integer and
+ - unregister lifting setup for Code_Numeral.integer and
Code_Numeral.natural
Potential INCOMPATIBILITY.
- Lifting.invariant -> eq_onp
INCOMPATIBILITY.
-
+
* New internal SAT solver "cdclite" that produces models and proof
traces. This solver replaces the internal SAT solvers "enumerate" and
"dpll". Applications that explicitly used one of these two SAT
@@ -806,9 +806,8 @@
* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
is subsumed by session Kleene_Algebra in AFP.
-* HOL-Library: RBT.thy: various constants and facts are hidden;
- lifting setup is unregistered
- INCOMPATIBILITY.
+* HOL-Library / theory RBT: various constants and facts are hidden;
+lifting setup is unregistered. INCOMPATIBILITY.
* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.