--- a/NEWS Thu Aug 06 10:47:13 1998 +0200
+++ b/NEWS Thu Aug 06 10:50:44 1998 +0200
@@ -93,7 +93,7 @@
*** HOL ***
* HOL/inductive package reorganized and improved: now supports mutual
-definitions such as:
+definitions such as
inductive EVEN ODD
intrs
@@ -111,7 +111,7 @@
* HOL/datatype package re-implemented and greatly improved: now
-supports mutually recursive datatypes such as:
+supports mutually recursive datatypes such as
datatype
'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
@@ -123,7 +123,7 @@
| AND ('a bexp) ('a bexp)
| OR ('a bexp) ('a bexp)
-as well as indirectly recursive datatypes such as:
+as well as indirectly recursive datatypes such as
datatype
('a, 'b) term = Var 'a
@@ -185,6 +185,8 @@
* HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
makes more sense);
+* HOL/Set INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name was misleading);
+
* HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
to 'converse' from 'inverse' (for compatibility with ZF and some
literature);
@@ -210,9 +212,6 @@
* HOL/Relation: renamed the relational operator r^-1 "converse"
instead of "inverse";
-* HOL/Set: added the predicate "disjoint A B" that stands for "A <= Compl B".
- This is much better than "A Int B = {}" for Fast/Blast_tac.
-
* directory HOL/Real: a construction of the reals using Dedekind cuts
(not included by default);
@@ -226,6 +225,11 @@
* theory Main includes everything;
+* ZF INCOMPATIBILITY: rule `equals0D' is now called `equals0E' (the old name
+ was misleading). The rule and 'sym RS equals0E' are now in the default
+ claset, giving automatic disjointness reasoning but breaking a few old
+ proofs.
+
* ZF/Update: new theory of function updates
with default rewrite rule f(x:=y) ` z = if(z=x, y, f`z)
may also be iterated as in f(a:=b,c:=d,...);