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

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