author | nipkow |

Fri May 01 11:43:38 1998 +0200 (1998-05-01) | |

changeset 4880 | 312115d20c45 |

parent 4879 | 58656c6a3551 |

child 4881 | d80faf83c82f |

*** empty log message ***

1.1 --- a/NEWS Fri May 01 11:23:04 1998 +0200 1.2 +++ b/NEWS Fri May 01 11:43:38 1998 +0200 1.3 @@ -7,6 +7,16 @@ 1.4 1.5 *** General Changes *** 1.6 1.7 +* Simplifier: 1.8 + 1.9 + -Asm_full_simp_tac is now more aggressive: 1.10 + 1. It will sometimes reorient premises if that increases their power to 1.11 + simplify. 1.12 + 2. It does no longer proceed strictly from left to right but may also 1.13 + rotate premises to achieve further simplification. 1.14 + For compatibility reasons there is now Asm_lr_simp_tac which is like the 1.15 + old Asm_full_simp_tac in that it does not rotate premises. 1.16 + 1.17 * Changed wrapper mechanism for the classical reasoner now allows for 1.18 selected deletion of wrappers, by introduction of names for wrapper 1.19 functionals. This implies that addbefore, addSbefore, addaltern, and 1.20 @@ -64,34 +74,26 @@ 1.21 * recdef can now declare non-recursive functions, with {} supplied as 1.22 the well-founded relation; 1.23 1.24 +* expand_if, expand_split, expand_sum_case and expand_nat_case are now called 1.25 + split_if, split_split, split_sum_case and split_nat_case 1.26 + (to go with add/delsplits). 1.27 + 1.28 * Simplifier: 1.29 1.30 -Rewrite rules for case distinctions can now be added permanently to the 1.31 default simpset using Addsplits just like Addsimps. They can be removed via 1.32 Delsplits just like Delsimps. Lower-case versions are also available. 1.33 1.34 - -The rule expand_if is now part of the default simpset. This means that 1.35 + -The rule split_if is now part of the default simpset. This means that 1.36 the simplifier will eliminate all ocurrences of if-then-else in the 1.37 - conclusion of a goal. To prevent this, you can either remove expand_if 1.38 - completely from the default simpset by `Delsplits [expand_if]' or 1.39 + conclusion of a goal. To prevent this, you can either remove split_if 1.40 + completely from the default simpset by `Delsplits [split_if]' or 1.41 remove it in a specific call of the simplifier using 1.42 - `... delsplits [expand_if]'. 1.43 + `... delsplits [split_if]'. 1.44 You can also add/delete other case splitting rules to/from the default 1.45 simpset: every datatype generates a suitable rule `split_t_case' (where t 1.46 is the name of the datatype). 1.47 1.48 - -Asm_full_simp_tac is now more aggressive: 1.49 - 1. It will sometimes reorient premises if that increases their power to 1.50 - simplify. 1.51 - 2. It does no longer proceed strictly from left to right but may also 1.52 - rotate premises to achieve further simplification. 1.53 - For compatibility reasons there is now Asm_lr_simp_tac which is like the 1.54 - old Asm_full_simp_tac in that it does not rotate premises. 1.55 - 1.56 -* expand_if, expand_split, expand_sum_case and expand_nat_case are now called 1.57 - split_if, split_split, split_sum_case and split_nat_case 1.58 - (to go with add/delsplits). 1.59 - 1.60 * new theory Vimage (inverse image of a function, syntax f-``B); 1.61 1.62 * many new identities for unions, intersections, set difference, etc.;