NEWS
 changeset 47496 a43f207f216f parent 47495 573ca05db948 child 47549 d19ce7f40d78
```     1.1 --- a/NEWS	Mon Apr 16 19:01:57 2012 +0200
1.2 +++ b/NEWS	Mon Apr 16 19:38:48 2012 +0200
1.3 @@ -129,7 +129,6 @@
1.4
1.5  *** HOL ***
1.6
1.7 -
1.8  * New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove").
1.9  It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
1.10  which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
1.11 @@ -138,30 +137,6 @@
1.12
1.13  * Discontinued old Tutorial on Isar ("isar-overview");
1.14
1.15 -* The representation of numerals has changed. We now have a datatype
1.16 -"num" representing strictly positive binary numerals, along with
1.17 -functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
1.18 -represent positive and negated numeric literals, respectively. (See
1.19 -definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories
1.20 -may require adaptations:
1.21 -
1.22 -  - Theorems with number_ring or number_semiring constraints: These
1.23 -    classes are gone; use comm_ring_1 or comm_semiring_1 instead.
1.24 -
1.25 -  - Theories defining numeric types: Remove number, number_semiring,
1.26 -    and number_ring instances. Defer all theorems about numerals until
1.27 -    after classes one and semigroup_add have been instantiated.
1.28 -
1.29 -  - Numeral-only simp rules: Replace each rule having a "number_of v"
1.30 -    pattern with two copies, one for numeral and one for neg_numeral.
1.31 -
1.32 -  - Theorems about subclasses of semiring_1 or ring_1: These classes
1.33 -    automatically support numerals now, so more simp rules and
1.34 -    simprocs may now apply within the proof.
1.35 -
1.36 -  - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
1.37 -    Redefine using other integer operations.
1.38 -
1.39  * Type 'a set is now a proper type constructor (just as before
1.40  Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
1.41  Non-trivial INCOMPATIBILITY.  For developments keeping predicates and
```