NEWS
changeset 57418 6ab1c7cb0b8d
parent 57415 e721124f1b1e
child 57423 96f970d1522b
     1.1 --- a/NEWS	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/NEWS	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -375,6 +375,75 @@
     1.4  * Theory reorganizations:
     1.5    * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
     1.6  
     1.7 +* Consolidated some facts about big group operators:
     1.8 +
     1.9 +    setsum_0' ~> setsum.neutral
    1.10 +    setsum_0 ~> setsum.neutral_const
    1.11 +    setsum_addf ~> setsum.distrib
    1.12 +    setsum_cartesian_product ~> setsum.cartesian_product
    1.13 +    setsum_cases ~> setsum.If_cases
    1.14 +    setsum_commute ~> setsum.commute
    1.15 +    setsum_cong ~> setsum.cong
    1.16 +    setsum_delta ~> setsum.delta
    1.17 +    setsum_delta' ~> setsum.delta'
    1.18 +    setsum_diff1' ~> setsum.remove
    1.19 +    setsum_empty ~> setsum.empty
    1.20 +    setsum_infinite ~> setsum.infinite
    1.21 +    setsum_insert ~> setsum.insert
    1.22 +    setsum_inter_restrict'' ~> setsum.inter_filter
    1.23 +    setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
    1.24 +    setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
    1.25 +    setsum_mono_zero_left ~> setsum.mono_neutral_left
    1.26 +    setsum_mono_zero_right ~> setsum.mono_neutral_right
    1.27 +    setsum_reindex ~> setsum.reindex
    1.28 +    setsum_reindex_cong ~> setsum.reindex_cong
    1.29 +    setsum_reindex_nonzero ~> setsum.reindex_nontrivial
    1.30 +    setsum_restrict_set ~> setsum.inter_restrict
    1.31 +    setsum_Plus ~> setsum.Plus
    1.32 +    setsum_setsum_restrict ~> setsum.commute_restrict
    1.33 +    setsum_Sigma ~> setsum.Sigma
    1.34 +    setsum_subset_diff ~> setsum.subset_diff
    1.35 +    setsum_Un_disjoint ~> setsum.union_disjoint
    1.36 +    setsum_UN_disjoint ~> setsum.UNION_disjoint
    1.37 +    setsum_Un_Int ~> setsum.union_inter
    1.38 +    setsum_Union_disjoint ~> setsum.Union_disjoint
    1.39 +    setsum_UNION_zero ~> setsum.Union_comp
    1.40 +    setsum_Un_zero ~> setsum.union_inter_neutral
    1.41 +    strong_setprod_cong ~> setprod.strong_cong
    1.42 +    strong_setsum_cong ~> setsum.strong_cong
    1.43 +    setprod_1' ~> setprod.neutral
    1.44 +    setprod_1 ~> setprod.neutral_const
    1.45 +    setprod_cartesian_product ~> setprod.cartesian_product
    1.46 +    setprod_cong ~> setprod.cong
    1.47 +    setprod_delta ~> setprod.delta
    1.48 +    setprod_delta' ~> setprod.delta'
    1.49 +    setprod_empty ~> setprod.empty
    1.50 +    setprod_infinite ~> setprod.infinite
    1.51 +    setprod_insert ~> setprod.insert
    1.52 +    setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left
    1.53 +    setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right
    1.54 +    setprod_mono_one_left ~> setprod.mono_neutral_left
    1.55 +    setprod_mono_one_right ~> setprod.mono_neutral_right
    1.56 +    setprod_reindex ~> setprod.reindex
    1.57 +    setprod_reindex_cong ~> setprod.reindex_cong
    1.58 +    setprod_reindex_nonzero ~> setprod.reindex_nontrivial
    1.59 +    setprod_Sigma ~> setprod.Sigma
    1.60 +    setprod_subset_diff ~> setprod.subset_diff
    1.61 +    setprod_timesf ~> setprod.distrib
    1.62 +    setprod_Un2 ~> setprod.union_diff2
    1.63 +    setprod_Un_disjoint ~> setprod.union_disjoint
    1.64 +    setprod_UN_disjoint ~> setprod.UNION_disjoint
    1.65 +    setprod_Un_Int ~> setprod.union_inter
    1.66 +    setprod_Union_disjoint ~> setprod.Union_disjoint
    1.67 +    setprod_Un_one ~> setprod.union_inter_neutral
    1.68 +
    1.69 +  Dropped setsum_cong2 (simple variant of setsum.cong).
    1.70 +  Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)
    1.71 +  Dropped setsum_reindex_id, setprod_reindex_id
    1.72 +    (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).
    1.73 +
    1.74 +  INCOMPATIBILITY.
    1.75 +
    1.76  * New internal SAT solver "cdclite" that produces models and proof traces.
    1.77    This solver replaces the internal SAT solvers "enumerate" and "dpll".
    1.78    Applications that explicitly used one of these two SAT solvers should