--- a/NEWS Tue Jul 18 21:44:42 2000 +0200
+++ b/NEWS Wed Jul 19 10:55:50 2000 +0200
@@ -41,10 +41,10 @@
Lfp, Gfp, WF); this only affects ML packages that refer to const names
internally;
-* Isar: changed syntax of local blocks from {{ }} to { };
+* HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
+ A/r to A//r;
-* FOL, ZF: AddIffs now available, giving theorems of the form P<->Q to the
- simplifier and classical reasoner simultaneously;
+* Isar: changed syntax of local blocks from {{ }} to { };
* Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
[| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
@@ -239,6 +239,12 @@
case of overlap with user translations (e.g. judgements over tuples);
+*** FOL & ZF ***
+
+* AddIffs now available, giving theorems of the form P<->Q to the
+ simplifier and classical reasoner simultaneously;
+
+
*** General ***
* AST translation rules no longer require constant head on LHS;