author | nipkow |

Fri Oct 16 17:36:12 1998 +0200 (1998-10-16) | |

changeset 5657 | 1a6c9c6a3f8e |

parent 5656 | f8389824189b |

child 5658 | 082debccf486 |

2. The simplifier now knows a little bit about nat-arithmetic.

1.1 --- a/NEWS Fri Oct 16 17:33:43 1998 +0200 1.2 +++ b/NEWS Fri Oct 16 17:36:12 1998 +0200 1.3 @@ -31,13 +31,15 @@ 1.4 1.5 *** Proof tools *** 1.6 1.7 -* Simplifier: Asm_full_simp_tac is now more aggressive. 1.8 - 1. It will sometimes reorient premises if that increases their power to 1.9 - simplify. 1.10 - 2. It does no longer proceed strictly from left to right but may also 1.11 - rotate premises to achieve further simplification. 1.12 - For compatibility reasons there is now Asm_lr_simp_tac which is like the 1.13 - old Asm_full_simp_tac in that it does not rotate premises. 1.14 +* Simplifier: 1.15 + 1. Asm_full_simp_tac is now more aggressive. 1.16 + 1. It will sometimes reorient premises if that increases their power to 1.17 + simplify. 1.18 + 2. It does no longer proceed strictly from left to right but may also 1.19 + rotate premises to achieve further simplification. 1.20 + For compatibility reasons there is now Asm_lr_simp_tac which is like the 1.21 + old Asm_full_simp_tac in that it does not rotate premises. 1.22 + 2. The simplifier now knows a little bit about nat-arithmetic. 1.23 1.24 * Classical reasoner: wrapper mechanism for the classical reasoner now 1.25 allows for selected deletion of wrappers, by introduction of names for