1.1 --- a/NEWS	Sat Apr 14 12:46:45 2012 +0200
     1.2 +++ b/NEWS	Sat Apr 14 12:51:38 2012 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  
     1.5  * Renamed facts about the power operation on relations, i.e., relpow
     1.6    to match the constant's name:
     1.7 -  
     1.8 +
     1.9    rel_pow_1 ~> relpow_1
    1.10    rel_pow_0_I ~> relpow_0_I
    1.11    rel_pow_Suc_I ~> relpow_Suc_I
    1.12 @@ -275,7 +275,7 @@
    1.13    rel_pow_Suc_E ~> relpow_Suc_E
    1.14    rel_pow_E ~> relpow_E
    1.15    rel_pow_Suc_D2 ~> relpow_Suc_D2
    1.16 -  rel_pow_Suc_E2 ~> relpow_Suc_E2 
    1.17 +  rel_pow_Suc_E2 ~> relpow_Suc_E2
    1.18    rel_pow_Suc_D2' ~> relpow_Suc_D2'
    1.19    rel_pow_E2 ~> relpow_E2
    1.20    rel_pow_add ~> relpow_add
    1.21 @@ -291,7 +291,7 @@
    1.22    rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow
    1.23    trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow
    1.24    single_valued_rel_pow ~> single_valued_relpow
    1.25 - 
    1.26 +
    1.27  INCOMPATIBILITY.
    1.28  
    1.29  * Theory Relation: Consolidated constant name for relation composition
    1.30 @@ -339,7 +339,7 @@
    1.31  use theory HOL/Library/Nat_Bijection instead.
    1.32  
    1.33  * Theory HOL/Library/RBT_Impl: Backing implementation of red-black trees is
    1.34 -now inside the type class' local context. Names of affected operations and lemmas 
    1.35 +now inside the type class' local context. Names of affected operations and lemmas
    1.36  have been prefixed by rbt_. INCOMPATIBILITY for theories working directly with
    1.37  raw red-black trees, adapt the names as follows:
    1.38  
    1.39 @@ -577,7 +577,7 @@
    1.40    - The command 'quickcheck_generator' creates random and exhaustive
    1.41      value generators for a given type and operations.
    1.42      It generates values by using the operations as if they were
    1.43 -    constructors of that type. 
    1.44 +    constructors of that type.
    1.45  
    1.46    - Support for multisets.
    1.47  
    1.48 @@ -600,7 +600,7 @@
    1.49  
    1.50  * SMT:
    1.51    - renamed "smt_fixed" option to "smt_read_only_certificates".
    1.52 - 
    1.53 +
    1.54  * Command 'try0':
    1.55    - Renamed from 'try_methods'. INCOMPATIBILITY.
    1.56  
    1.57 @@ -616,6 +616,16 @@
    1.58  * New "case_product" attribute (see HOL).
    1.59  
    1.60  
    1.61 +*** ZF ***
    1.62 +
    1.63 +* Greater support for structured proofs involving induction or case
    1.64 +analysis.
    1.65 +
    1.66 +* Much greater use of mathematical symbols.
    1.67 +
    1.68 +* Removal of many ML theorem bindings.  INCOMPATIBILITY.
    1.69 +
    1.70 +
    1.71  *** ML ***
    1.72  
    1.73  * Antiquotation @{keyword "name"} produces a parser for outer syntax
    1.74 @@ -1978,13 +1988,6 @@
    1.75  * All constant names are now qualified internally and use proper
    1.76  identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
    1.77  
    1.78 -*** ZF ***
    1.79 -
    1.80 -* Greater support for structured proofs involving induction or case analysis.
    1.81 -
    1.82 -* Much greater use of special symbols.
    1.83 -
    1.84 -* Removal of many ML theorem bindings. INCOMPATIBILITY.
    1.85  
    1.86  *** ML ***
    1.87  
    1.88 @@ -5076,7 +5079,7 @@
    1.89  * HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
    1.90  
    1.91  * HOL-Word: New extensive library and type for generic, fixed size
    1.92 -machine words, with arithmetic, bit-wise, shifting and rotating
    1.93 +machine words, with arithemtic, bit-wise, shifting and rotating
    1.94  operations, reflection into int, nat, and bool lists, automation for
    1.95  linear arithmetic (by automatic reflection into nat or int), including
    1.96  lemmas on overflow and monotonicity.  Instantiated to all appropriate