# HG changeset patch # User haftmann # Date 1272357761 -7200 # Node ID 9459be72b89eb293c7d9fee4f073d5d547ad42a6 # Parent a168ac750096dc2cf4988d0e7db06b7baed78d6b NEWS and CONTRIBUTORS diff -r a168ac750096 -r 9459be72b89e CONTRIBUTORS --- a/CONTRIBUTORS Tue Apr 27 09:49:40 2010 +0200 +++ b/CONTRIBUTORS Tue Apr 27 10:42:41 2010 +0200 @@ -6,6 +6,14 @@ Contributions to this Isabelle version -------------------------------------- +* April 2010, Florian Haftmann, TUM + Reorganization of abstract algebra type classes. + +* April 2010, Florian Haftmann, TUM + Code generation for data representations involving invariants; + various collections avaiable in theories Fset, Dlist, RBT, + Mapping and AssocList. + Contributions to Isabelle2009-1 ------------------------------- diff -r a168ac750096 -r 9459be72b89e NEWS --- a/NEWS Tue Apr 27 09:49:40 2010 +0200 +++ b/NEWS Tue Apr 27 10:42:41 2010 +0200 @@ -121,17 +121,6 @@ *** HOL *** -* Abstract algebra: - * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero - include rule inverse 0 = 0 -- subsumes former division_by_zero class. - * numerous lemmas have been ported from field to division_ring; - * dropped theorem group group_simps, use algebra_simps instead; - * dropped theorem group ring_simps, use field_simps instead; - * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps; - * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero. - - INCOMPATIBILITY. - * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT' provides abstract red-black tree type which is backed by RBT_Impl as implementation. INCOMPATIBILTY. @@ -160,16 +149,11 @@ INCOMPATIBILITY. * Some generic constants have been put to appropriate theories: - - less_eq, less: Orderings - zero, one, plus, minus, uminus, times, abs, sgn: Groups - inverse, divide: Rings - + * less_eq, less: Orderings + * zero, one, plus, minus, uminus, times, abs, sgn: Groups + * inverse, divide: Rings INCOMPATIBILITY. -* Class division_ring also requires proof of fact divide_inverse. However instantiation -of parameter divide has also been required previously. INCOMPATIBILITY. - * More consistent naming of type classes involving orderings (and lattices): lower_semilattice ~> semilattice_inf @@ -221,33 +205,18 @@ INCOMPATIBILITY. -* HOLogic.strip_psplit: types are returned in syntactic order, similar -to other strip and tuple operations. INCOMPATIBILITY. - -* Various old-style primrec specifications in the HOL theories have been -replaced by new-style primrec, especially in theory List. The corresponding -constants now have authentic syntax. INCOMPATIBILITY. - -* Reorganized theory Multiset: swapped notation of pointwise and multiset order: - * pointwise ordering is instance of class order with standard syntax <= and <; - * multiset ordering has syntax <=# and <#; partial order properties are provided - by means of interpretation with prefix multiset_order. -Less duplication, less historical organization of sections, -conversion from associations lists to multisets, rudimentary code generation. -Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed. -INCOMPATIBILITY. - -* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax. -INCOMPATIBILITY. - -* Code generation: ML and OCaml code is decorated with signatures. - -* Theory Complete_Lattice: lemmas top_def and bot_def have been -replaced by the more convenient lemmas Inf_empty and Sup_empty. -Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed -by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace -former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right -subsume inf_top and sup_bot respectively. INCOMPATIBILITY. +* Refined field classes: + * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero + include rule inverse 0 = 0 -- subsumes former division_by_zero class. + * numerous lemmas have been ported from field to division_ring; + INCOMPATIBILITY. + +* Refined algebra theorem collections: + * dropped theorem group group_simps, use algebra_simps instead; + * dropped theorem group ring_simps, use field_simps instead; + * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps; + * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero. + INCOMPATIBILITY. * Theory Finite_Set and List: some lemmas have been generalized from sets to lattices: @@ -263,6 +232,27 @@ INTER_fold_inter ~> INFI_fold_inf UNION_fold_union ~> SUPR_fold_sup +* Theory Complete_Lattice: lemmas top_def and bot_def have been +replaced by the more convenient lemmas Inf_empty and Sup_empty. +Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed +by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace +former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right +subsume inf_top and sup_bot respectively. INCOMPATIBILITY. + +* HOLogic.strip_psplit: types are returned in syntactic order, similar +to other strip and tuple operations. INCOMPATIBILITY. + +* Reorganized theory Multiset: swapped notation of pointwise and multiset order: + * pointwise ordering is instance of class order with standard syntax <= and <; + * multiset ordering has syntax <=# and <#; partial order properties are provided + by means of interpretation with prefix multiset_order; + * less duplication, less historical organization of sections, + conversion from associations lists to multisets, rudimentary code generation; + * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed. + INCOMPATIBILITY. + +* Code generation: ML and OCaml code is decorated with signatures. + * Theory List: added transpose. * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid