author | nipkow |
Wed, 27 Jun 2007 11:06:43 +0200 | |
changeset 23509 | 14a2f87ccc73 |
parent 23508 | 702e27cabe82 |
child 23510 | 4521fead5609 |
--- a/NEWS Tue Jun 26 18:32:53 2007 +0200 +++ b/NEWS Wed Jun 27 11:06:43 2007 +0200 @@ -610,6 +610,9 @@ * Lemma collections ring_eq_simps, group_eq_simps and ring_distrib have been improved and renamed to ring_simps, group_simps and ring_distribs. + Removed lemmas field_xyz in Ring_and_Field + because they were subsumed by lemmas xyz. +INCOMPATIBILITY. * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals when generating code.