summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.12 +may require adaptations: 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