ZF/Simplifier: second copy of context type solver;
authorwenzelm
Fri Jul 30 10:42:19 2004 +0200 (2004-07-30)
changeset 15089430264838064
parent 15088 b8a95eadbc14
child 15090 970c2668c694
ZF/Simplifier: second copy of context type solver;
NEWS
     1.1 --- a/NEWS	Fri Jul 30 10:41:52 2004 +0200
     1.2 +++ b/NEWS	Fri Jul 30 10:42:19 2004 +0200
     1.3 @@ -187,12 +187,12 @@
     1.4    Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
     1.5    now translates into 'setsum' as above.
     1.6  
     1.7 -* Simplifier:
     1.8 -  - Is now set up to reason about transitivity chains involving "trancl" (r^+)
     1.9 -    and "rtrancl" (r^*) by setting up tactics provided by Provers/trancl.ML
    1.10 -    as additional solvers.
    1.11 -  - INCOMPATIBILITY: old proofs break occasionally.  Typically, this is
    1.12 -    because simplification now solves more goals than previously.
    1.13 +* HOL/Simplifier: Is now set up to reason about transitivity chains
    1.14 +  involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
    1.15 +  provided by Provers/trancl.ML as additional solvers.
    1.16 +  INCOMPATIBILITY: old proofs break occasionally as simplification may
    1.17 +  now solve more goals than previously.
    1.18 +
    1.19  
    1.20  *** HOLCF ***
    1.21  
    1.22 @@ -203,8 +203,13 @@
    1.23  
    1.24  *** ZF ***
    1.25  
    1.26 -* ZF/ex/{Group,Ring}: examples in abstract algebra, including the First
    1.27 -  Isomorphism Theorem (on quotienting by the kernel of a homomorphism).
    1.28 +* ZF/ex/{Group,Ring}: examples in abstract algebra, including the
    1.29 +  First Isomorphism Theorem (on quotienting by the kernel of a
    1.30 +  homomorphism).
    1.31 +
    1.32 +* ZF/Simplifier: install second copy of type solver that actually
    1.33 +  makes use of TC rules declared to Isar proof contexts (or locales);
    1.34 +  the old version is still required for ML proof scripts.
    1.35  
    1.36  
    1.37