# HG changeset patch
# User paulson
# Date 900667520 -7200
# Node ID 1ff6679144b90e3fca1ed3a6bb82a8856eb4f27c
# Parent  8fc4fb20d70f3e127a06496d642fd925b99947ce
ZF: Main, Update

diff -r 8fc4fb20d70f -r 1ff6679144b9 NEWS
--- a/NEWS	Fri Jul 17 11:24:09 1998 +0200
+++ b/NEWS	Fri Jul 17 11:25:20 1998 +0200
@@ -9,6 +9,10 @@
 * HOL/inductive requires Inductive.thy as an ancestor;
 * `inj_onto' is now called `inj_on' (which makes more sense)
 
+* HOL/Relation: renamed the relational operator r^-1 to 'converse'
+  from 'inverse' (for compatibility with ZF and some literature)
+
+
 *** Proof tools ***
 
 * Simplifier: Asm_full_simp_tac is now more aggressive.
@@ -157,11 +161,20 @@
 
 *** ZF ***
 
+* theory Main includes everything;
+
+* 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,...);
+
 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
 
 * calling (stac rew i) now fails if "rew" has no effect on the goal
   [previously, this check worked only if the rewrite rule was unconditional]
 
+* case_tac provided for compatibility with HOL
+    (like the old excluded_middle_tac, but with subgoals swapped)
+
 
 *** Internal programming interfaces ***