# HG changeset patch
# User wenzelm
# Date 1334597928 -7200
# Node ID a43f207f216f82f2a8c3bf2a79163e999cd9a91e
# Parent  573ca05db948797b69b8c111c59e5db80ad96c47
repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1);

diff -r 573ca05db948 -r a43f207f216f NEWS
--- a/NEWS	Mon Apr 16 19:01:57 2012 +0200
+++ b/NEWS	Mon Apr 16 19:38:48 2012 +0200
@@ -129,7 +129,6 @@
 
 *** HOL ***
 
-
 * New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove").
 It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
 which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
@@ -138,30 +137,6 @@
 
 * Discontinued old Tutorial on Isar ("isar-overview");
 
-* The representation of numerals has changed. We now have a datatype
-"num" representing strictly positive binary numerals, along with
-functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
-represent positive and negated numeric literals, respectively. (See
-definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories
-may require adaptations:
-
-  - Theorems with number_ring or number_semiring constraints: These
-    classes are gone; use comm_ring_1 or comm_semiring_1 instead.
-
-  - Theories defining numeric types: Remove number, number_semiring,
-    and number_ring instances. Defer all theorems about numerals until
-    after classes one and semigroup_add have been instantiated.
-
-  - Numeral-only simp rules: Replace each rule having a "number_of v"
-    pattern with two copies, one for numeral and one for neg_numeral.
-
-  - Theorems about subclasses of semiring_1 or ring_1: These classes
-    automatically support numerals now, so more simp rules and
-    simprocs may now apply within the proof.
-
-  - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
-    Redefine using other integer operations.
-
 * Type 'a set is now a proper type constructor (just as before
 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.
 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and