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