NEWS
 changeset 54264 27501a51d847 parent 54250 7d2544dd3988 child 54295 45a5523d4a63
equal inserted replaced
54263:c4159fe6fa46 54264:27501a51d847
`    12 `
`    12 `
`    13 * Purely algebraic definition of even.  Fact generalization and consolidation:`
`    13 * Purely algebraic definition of even.  Fact generalization and consolidation:`
`    14     nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd`
`    14     nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd`
`    15     even_zero_(nat|int) ~> even_zero`
`    15     even_zero_(nat|int) ~> even_zero`
`    16 INCOMPATIBILITY.`
`    16 INCOMPATIBILITY.`
`    19 `
`    17 `
`    20 * Elimination of fact duplicates:`
`    18 * Elimination of fact duplicates:`
`    21     equals_zero_I ~> minus_unique`
`    19     equals_zero_I ~> minus_unique`
`    22     diff_eq_0_iff_eq ~> right_minus_eq`
`    20     diff_eq_0_iff_eq ~> right_minus_eq`
`    23 INCOMPATIBILITY.`
`    21 INCOMPATIBILITY.`
`    49 `
`    47 `
`    50 c) Simplification with "diff_def": just drop "diff_def".`
`    48 c) Simplification with "diff_def": just drop "diff_def".`
`    51 Consider simplification with algebra_simps or field_simps;`
`    49 Consider simplification with algebra_simps or field_simps;`
`    52 or the brute way with`
`    50 or the brute way with`
`    53 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".`
`    51 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".`
`       `
`    52 `
`       `
`    53 * SUP and INF generalized to conditionally_complete_lattice`
`       `
`    54 `
`       `
`    55 * Theory Lubs moved HOL image to HOL-Library. It is replaced by`
`       `
`    56 Conditionally_Complete_Lattices.   INCOMPATIBILITY.`
`       `
`    57 `
`       `
`    58 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them`
`       `
`    59 instead of explicitly stating boundedness of sets.`
`       `
`    60 `
`    54 `
`    61 `
`    55 New in Isabelle2013-1 (November 2013)`
`    62 New in Isabelle2013-1 (November 2013)`
`    56 -------------------------------------`
`    63 -------------------------------------`
`    57 `
`    64 `
`    58 *** General ***`
`    65 *** General ***`