NEWS
 changeset 47108 2a1953f0d20d parent 47086 69276374c0a1 child 47113 b5a5662528fb
```     1.1 --- a/NEWS	Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/NEWS	Sun Mar 25 20:15:39 2012 +0200
1.3 @@ -90,6 +90,30 @@
1.4
1.5  *** HOL ***
1.6
1.7 +* The representation of numerals has changed. We now have a datatype
1.8 +"num" representing strictly positive binary numerals, along with
1.9 +functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
1.10 +represent positive and negated numeric literals, respectively. (See
1.11 +definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories
1.13 +
1.14 +  - Theorems with number_ring or number_semiring constraints: These
1.15 +    classes are gone; use comm_ring_1 or comm_semiring_1 instead.
1.16 +
1.17 +  - Theories defining numeric types: Remove number, number_semiring,
1.18 +    and number_ring instances. Defer all theorems about numerals until
1.19 +    after classes one and semigroup_add have been instantiated.
1.20 +
1.21 +  - Numeral-only simp rules: Replace each rule having a "number_of v"
1.22 +    pattern with two copies, one for numeral and one for neg_numeral.
1.23 +
1.24 +  - Theorems about subclasses of semiring_1 or ring_1: These classes
1.25 +    automatically support numerals now, so more simp rules and
1.26 +    simprocs may now apply within the proof.
1.27 +
1.28 +  - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
1.29 +    Redefine using other integer operations.
1.30 +
1.31  * Type 'a set is now a proper type constructor (just as before
1.32  Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
1.33  Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
```