# HG changeset patch
# User wenzelm
# Date 1091176939 -7200
# Node ID 4302648380640399385bd93081cce24934eb7567
# Parent  b8a95eadbc140ec4cf21cb2d14876d02756c8851
ZF/Simplifier: second copy of context type solver;

diff -r b8a95eadbc14 -r 430264838064 NEWS
--- a/NEWS	Fri Jul 30 10:41:52 2004 +0200
+++ b/NEWS	Fri Jul 30 10:42:19 2004 +0200
@@ -187,12 +187,12 @@
   Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
   now translates into 'setsum' as above.
 
-* Simplifier:
-  - Is now set up to reason about transitivity chains involving "trancl" (r^+)
-    and "rtrancl" (r^*) by setting up tactics provided by Provers/trancl.ML
-    as additional solvers.
-  - INCOMPATIBILITY: old proofs break occasionally.  Typically, this is
-    because simplification now solves more goals than previously.
+* HOL/Simplifier: Is now set up to reason about transitivity chains
+  involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
+  provided by Provers/trancl.ML as additional solvers.
+  INCOMPATIBILITY: old proofs break occasionally as simplification may
+  now solve more goals than previously.
+
 
 *** HOLCF ***
 
@@ -203,8 +203,13 @@
 
 *** ZF ***
 
-* ZF/ex/{Group,Ring}: examples in abstract algebra, including the First
-  Isomorphism Theorem (on quotienting by the kernel of a homomorphism).
+* ZF/ex/{Group,Ring}: examples in abstract algebra, including the
+  First Isomorphism Theorem (on quotienting by the kernel of a
+  homomorphism).
+
+* ZF/Simplifier: install second copy of type solver that actually
+  makes use of TC rules declared to Isar proof contexts (or locales);
+  the old version is still required for ML proof scripts.