NEWS and CONTRIBUTORS
authorhaftmann
Tue Apr 27 10:42:41 2010 +0200 (2010-04-27)
changeset 364169459be72b89e
parent 36415 a168ac750096
child 36417 54bc1a44967d
child 36422 69004340f53c
NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Apr 27 09:49:40 2010 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Apr 27 10:42:41 2010 +0200
     1.3 @@ -6,6 +6,14 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* April 2010, Florian Haftmann, TUM
     1.8 +  Reorganization of abstract algebra type classes.
     1.9 +
    1.10 +* April 2010, Florian Haftmann, TUM
    1.11 +  Code generation for data representations involving invariants;
    1.12 +  various collections avaiable in theories Fset, Dlist, RBT,
    1.13 +  Mapping and AssocList.
    1.14 +
    1.15  
    1.16  Contributions to Isabelle2009-1
    1.17  -------------------------------
     2.1 --- a/NEWS	Tue Apr 27 09:49:40 2010 +0200
     2.2 +++ b/NEWS	Tue Apr 27 10:42:41 2010 +0200
     2.3 @@ -121,17 +121,6 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 -* Abstract algebra:
     2.8 -  * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
     2.9 -    include rule inverse 0 = 0 -- subsumes former division_by_zero class.
    2.10 -  * numerous lemmas have been ported from field to division_ring;
    2.11 -  * dropped theorem group group_simps, use algebra_simps instead;
    2.12 -  * dropped theorem group ring_simps, use field_simps instead;
    2.13 -  * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps;
    2.14 -  * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
    2.15 -
    2.16 -  INCOMPATIBILITY.
    2.17 -
    2.18  * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
    2.19  provides abstract red-black tree type which is backed by RBT_Impl
    2.20  as implementation.  INCOMPATIBILTY.
    2.21 @@ -160,16 +149,11 @@
    2.22  INCOMPATIBILITY.
    2.23  
    2.24  * Some generic constants have been put to appropriate theories:
    2.25 -
    2.26 -    less_eq, less: Orderings
    2.27 -    zero, one, plus, minus, uminus, times, abs, sgn: Groups
    2.28 -    inverse, divide: Rings
    2.29 -
    2.30 +  * less_eq, less: Orderings
    2.31 +  * zero, one, plus, minus, uminus, times, abs, sgn: Groups
    2.32 +  * inverse, divide: Rings
    2.33  INCOMPATIBILITY.
    2.34  
    2.35 -* Class division_ring also requires proof of fact divide_inverse.  However instantiation
    2.36 -of parameter divide has also been required previously.  INCOMPATIBILITY.
    2.37 -
    2.38  * More consistent naming of type classes involving orderings (and lattices):
    2.39  
    2.40      lower_semilattice                   ~> semilattice_inf
    2.41 @@ -221,33 +205,18 @@
    2.42  
    2.43  INCOMPATIBILITY.
    2.44  
    2.45 -* HOLogic.strip_psplit: types are returned in syntactic order, similar
    2.46 -to other strip and tuple operations.  INCOMPATIBILITY.
    2.47 -
    2.48 -* Various old-style primrec specifications in the HOL theories have been
    2.49 -replaced by new-style primrec, especially in theory List.  The corresponding
    2.50 -constants now have authentic syntax.  INCOMPATIBILITY.
    2.51 -
    2.52 -* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
    2.53 -  * pointwise ordering is instance of class order with standard syntax <= and <;
    2.54 -  * multiset ordering has syntax <=# and <#; partial order properties are provided
    2.55 -      by means of interpretation with prefix multiset_order.
    2.56 -Less duplication, less historical organization of sections,
    2.57 -conversion from associations lists to multisets, rudimentary code generation.
    2.58 -Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
    2.59 -INCOMPATIBILITY.
    2.60 -
    2.61 -* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.
    2.62 -INCOMPATIBILITY.
    2.63 -
    2.64 -* Code generation: ML and OCaml code is decorated with signatures.
    2.65 -
    2.66 -* Theory Complete_Lattice: lemmas top_def and bot_def have been
    2.67 -replaced by the more convenient lemmas Inf_empty and Sup_empty.
    2.68 -Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
    2.69 -by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
    2.70 -former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
    2.71 -subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
    2.72 +* Refined field classes:
    2.73 +  * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
    2.74 +    include rule inverse 0 = 0 -- subsumes former division_by_zero class.
    2.75 +  * numerous lemmas have been ported from field to division_ring;
    2.76 +  INCOMPATIBILITY.
    2.77 +
    2.78 +* Refined algebra theorem collections:
    2.79 +  * dropped theorem group group_simps, use algebra_simps instead;
    2.80 +  * dropped theorem group ring_simps, use field_simps instead;
    2.81 +  * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps;
    2.82 +  * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
    2.83 +  INCOMPATIBILITY.
    2.84  
    2.85  * Theory Finite_Set and List: some lemmas have been generalized from
    2.86  sets to lattices:
    2.87 @@ -263,6 +232,27 @@
    2.88    INTER_fold_inter              ~> INFI_fold_inf
    2.89    UNION_fold_union              ~> SUPR_fold_sup
    2.90  
    2.91 +* Theory Complete_Lattice: lemmas top_def and bot_def have been
    2.92 +replaced by the more convenient lemmas Inf_empty and Sup_empty.
    2.93 +Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
    2.94 +by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
    2.95 +former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
    2.96 +subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
    2.97 +
    2.98 +* HOLogic.strip_psplit: types are returned in syntactic order, similar
    2.99 +to other strip and tuple operations.  INCOMPATIBILITY.
   2.100 +
   2.101 +* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
   2.102 +  * pointwise ordering is instance of class order with standard syntax <= and <;
   2.103 +  * multiset ordering has syntax <=# and <#; partial order properties are provided
   2.104 +      by means of interpretation with prefix multiset_order;
   2.105 +  * less duplication, less historical organization of sections,
   2.106 +      conversion from associations lists to multisets, rudimentary code generation;
   2.107 +  * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
   2.108 +  INCOMPATIBILITY.
   2.109 +
   2.110 +* Code generation: ML and OCaml code is decorated with signatures.
   2.111 +
   2.112  * Theory List: added transpose.
   2.113  
   2.114  * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid