1.1 --- a/NEWS	Thu Dec 05 17:52:12 2013 +0100
     1.2 +++ b/NEWS	Thu Dec 05 17:58:03 2013 +0100
     1.3 @@ -1,6 +1,98 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +New in this Isabelle version
     1.8 +----------------------------
     1.9 +
    1.10 +*** Prover IDE -- Isabelle/Scala/jEdit ***
    1.11 +
    1.12 +* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
    1.13 +Open text buffers take precedence over copies within the file-system.
    1.14 +
    1.15 +
    1.16 +*** HOL ***
    1.17 +
    1.18 +* Qualified constant names Wellfounded.acc, Wellfounded.accp.
    1.19 +INCOMPATIBILITY.
    1.20 +
    1.21 +* Fact generalization and consolidation:
    1.22 +    neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
    1.23 +INCOMPATIBILITY.
    1.24 +
    1.25 +* Purely algebraic definition of even.  Fact generalization and consolidation:
    1.26 +    nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
    1.27 +    even_zero_(nat|int) ~> even_zero
    1.28 +INCOMPATIBILITY.
    1.29 +
    1.30 +* Abolished neg_numeral.
    1.31 +  * Canonical representation for minus one is "- 1".
    1.32 +  * Canonical representation for other negative numbers is "- (numeral _)".
    1.33 +  * When devising rule sets for number calculation, consider the
    1.34 +    following canonical cases: 0, 1, numeral _, - 1, - numeral _.
    1.35 +  * HOLogic.dest_number also recognizes numerals in non-canonical forms
    1.36 +    like "numeral One", "- numeral One", "- 0" and even "- … - _".
    1.37 +  * Syntax for negative numerals is mere input syntax.
    1.38 +INCOMPATBILITY.
    1.39 +
    1.40 +* Elimination of fact duplicates:
    1.41 +    equals_zero_I ~> minus_unique
    1.42 +    diff_eq_0_iff_eq ~> right_minus_eq
    1.43 +    nat_infinite ~> infinite_UNIV_nat
    1.44 +    int_infinite ~> infinite_UNIV_int
    1.45 +INCOMPATIBILITY.
    1.46 +
    1.47 +* Fact name consolidation:
    1.48 +    diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
    1.49 +    minus_le_self_iff ~> neg_less_eq_nonneg
    1.50 +    le_minus_self_iff ~> less_eq_neg_nonpos
    1.51 +    neg_less_nonneg ~> neg_less_pos
    1.52 +    less_minus_self_iff ~> less_neg_neg [simp]
    1.53 +INCOMPATIBILITY.
    1.54 +
    1.55 +* More simplification rules on unary and binary minus:
    1.56 +add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
    1.57 +add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
    1.58 +add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
    1.59 +le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
    1.60 +minus_add_cancel, uminus_add_conv_diff.  These correspondingly
    1.61 +have been taken away from fact collections algebra_simps and
    1.62 +field_simps.  INCOMPATIBILITY.
    1.63 +
    1.64 +To restore proofs, the following patterns are helpful:
    1.65 +
    1.66 +a) Arbitrary failing proof not involving "diff_def":
    1.67 +Consider simplification with algebra_simps or field_simps.
    1.68 +
    1.69 +b) Lifting rules from addition to subtraction:
    1.70 +Try with "using <rule for addition> of [… "- _" …]" by simp".
    1.71 +
    1.72 +c) Simplification with "diff_def": just drop "diff_def".
    1.73 +Consider simplification with algebra_simps or field_simps;
    1.74 +or the brute way with
    1.75 +"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
    1.76 +
    1.77 +* SUP and INF generalized to conditionally_complete_lattice
    1.78 +
    1.79 +* Theory Lubs moved HOL image to HOL-Library. It is replaced by
    1.80 +Conditionally_Complete_Lattices.   INCOMPATIBILITY.
    1.81 +
    1.82 +* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
    1.83 +instead of explicitly stating boundedness of sets.
    1.84 +
    1.85 +* ccpo.admissible quantifies only over non-empty chains to allow
    1.86 +more syntax-directed proof rules; the case of the empty chain
    1.87 +shows up as additional case in fixpoint induction proofs.
    1.88 +INCOMPATIBILITY
    1.89 +
    1.90 +*** ML ***
    1.91 +
    1.92 +* Toplevel function "use" refers to raw ML bootstrap environment,
    1.93 +without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
    1.94 +Note that 'ML_file' is the canonical command to load ML files into the
    1.95 +formal context.
    1.96 +
    1.97 +
    1.98 +
    1.99  New in Isabelle2013-2 (December 2013)
   1.100  -------------------------------------
   1.101  
   1.102 @@ -457,6 +549,10 @@
   1.103      sets ~> set
   1.104  IMCOMPATIBILITY.
   1.105  
   1.106 +* Nitpick:
   1.107 +  - Fixed soundness bug whereby mutually recursive datatypes could take
   1.108 +    infinite values.
   1.109 +
   1.110  
   1.111  *** ML ***
   1.112