# HG changeset patch
# User wenzelm
# Date 1334400698 -7200
# Node ID 9be52539082de657325f87720f505be065326c02
# Parent  8f85051693d141fa1074ad658390c46cde7c5c71
revert changes of already published NEWS;

diff -r 8f85051693d1 -r 9be52539082d NEWS
--- a/NEWS	Sat Apr 14 12:46:45 2012 +0200
+++ b/NEWS	Sat Apr 14 12:51:38 2012 +0200
@@ -266,7 +266,7 @@
 
 * Renamed facts about the power operation on relations, i.e., relpow
   to match the constant's name:
-  
+
   rel_pow_1 ~> relpow_1
   rel_pow_0_I ~> relpow_0_I
   rel_pow_Suc_I ~> relpow_Suc_I
@@ -275,7 +275,7 @@
   rel_pow_Suc_E ~> relpow_Suc_E
   rel_pow_E ~> relpow_E
   rel_pow_Suc_D2 ~> relpow_Suc_D2
-  rel_pow_Suc_E2 ~> relpow_Suc_E2 
+  rel_pow_Suc_E2 ~> relpow_Suc_E2
   rel_pow_Suc_D2' ~> relpow_Suc_D2'
   rel_pow_E2 ~> relpow_E2
   rel_pow_add ~> relpow_add
@@ -291,7 +291,7 @@
   rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow
   trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow
   single_valued_rel_pow ~> single_valued_relpow
- 
+
 INCOMPATIBILITY.
 
 * Theory Relation: Consolidated constant name for relation composition
@@ -339,7 +339,7 @@
 use theory HOL/Library/Nat_Bijection instead.
 
 * Theory HOL/Library/RBT_Impl: Backing implementation of red-black trees is
-now inside the type class' local context. Names of affected operations and lemmas 
+now inside the type class' local context. Names of affected operations and lemmas
 have been prefixed by rbt_. INCOMPATIBILITY for theories working directly with
 raw red-black trees, adapt the names as follows:
 
@@ -577,7 +577,7 @@
   - The command 'quickcheck_generator' creates random and exhaustive
     value generators for a given type and operations.
     It generates values by using the operations as if they were
-    constructors of that type. 
+    constructors of that type.
 
   - Support for multisets.
 
@@ -600,7 +600,7 @@
 
 * SMT:
   - renamed "smt_fixed" option to "smt_read_only_certificates".
- 
+
 * Command 'try0':
   - Renamed from 'try_methods'. INCOMPATIBILITY.
 
@@ -616,6 +616,16 @@
 * New "case_product" attribute (see HOL).
 
 
+*** ZF ***
+
+* Greater support for structured proofs involving induction or case
+analysis.
+
+* Much greater use of mathematical symbols.
+
+* Removal of many ML theorem bindings.  INCOMPATIBILITY.
+
+
 *** ML ***
 
 * Antiquotation @{keyword "name"} produces a parser for outer syntax
@@ -1978,13 +1988,6 @@
 * All constant names are now qualified internally and use proper
 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
 
-*** ZF ***
-
-* Greater support for structured proofs involving induction or case analysis.
-
-* Much greater use of special symbols.
-
-* Removal of many ML theorem bindings. INCOMPATIBILITY.
 
 *** ML ***
 
@@ -5076,7 +5079,7 @@
 * HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
 
 * HOL-Word: New extensive library and type for generic, fixed size
-machine words, with arithmetic, bit-wise, shifting and rotating
+machine words, with arithemtic, bit-wise, shifting and rotating
 operations, reflection into int, nat, and bool lists, automation for
 linear arithmetic (by automatic reflection into nat or int), including
 lemmas on overflow and monotonicity.  Instantiated to all appropriate