summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 23480 | 8d01ccdc3652 |

parent 23478 | 26a5ef187e8b |

child 23481 | 93dca7620d0d |

1.1 --- a/NEWS Sun Jun 24 15:17:54 2007 +0200 1.2 +++ b/NEWS Sun Jun 24 20:18:20 2007 +0200 1.3 @@ -603,17 +603,22 @@ 1.4 [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, 1.5 and for uniformity. INCOMPATIBILITY 1.6 1.7 -* The lemma collections ring_eq_simps, group_eq_simps and ring_distrib 1.8 +* New lemma collection field_simps (an extension of ring_simps) 1.9 + for manipulating (in)equations involving division. Multiplies 1.10 + with all denominators which can be proved to be non-zero (in equations) 1.11 + or positive/negative (in inequations). 1.12 + 1.13 +* Lemma collections ring_eq_simps, group_eq_simps and ring_distrib 1.14 have been improved and renamed to ring_simps, group_simps and ring_distribs. 1.15 1.16 * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals 1.17 - when generating code. 1.18 + when generating code. 1.19 1.20 * Library/Pretty_Char.thy: maps HOL characters on target language character literals 1.21 - when generating code. 1.22 + when generating code. 1.23 1.24 * Library/Commutative_Ring.thy: switched from recdef to function package; 1.25 - constants add, mul, pow now curried. Infix syntax for algebraic operations. 1.26 + constants add, mul, pow now curried. Infix syntax for algebraic operations. 1.27 1.28 * Some steps towards more uniform lattice theory development in HOL. 1.29