| changeset 33361 | 1f18de40b43f |
| parent 33273 | 9290fbf0a30e |
| child 33419 | 8ae45e87b992 |
--- a/NEWS Fri Oct 30 13:59:52 2009 +0100 +++ b/NEWS Fri Oct 30 14:00:43 2009 +0100 @@ -37,6 +37,11 @@ *** HOL *** +* Combined former theories Divides and IntDiv to one theory Divides +in the spirit of other number theory theories in HOL; some constants +(and to a lesser extent also facts) have been suffixed with _nat und _int +respectively. INCOMPATIBILITY. + * Most rules produced by inductive and datatype package have mandatory prefixes. INCOMPATIBILITY.