author | nipkow |
Sun, 24 Jun 2007 10:33:49 +0200 | |
changeset 23478 | 26a5ef187e8b |
parent 23477 | f4b83f03cac9 |
child 23479 | 10adbdcdc65b |
--- a/NEWS Sat Jun 23 19:33:22 2007 +0200 +++ b/NEWS Sun Jun 24 10:33:49 2007 +0200 @@ -603,6 +603,9 @@ [x <- xs. P] to avoid an ambiguity caused by list comprehension syntax, and for uniformity. INCOMPATIBILITY +* The lemma collections ring_eq_simps, group_eq_simps and ring_distrib + have been improved and renamed to ring_simps, group_simps and ring_distribs. + * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals when generating code.