author | wenzelm |

Fri Jul 30 10:42:19 2004 +0200 (2004-07-30) | |

changeset 15089 | 430264838064 |

parent 15088 | b8a95eadbc14 |

child 15090 | 970c2668c694 |

ZF/Simplifier: second copy of context type solver;

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