author | haftmann |

Tue Apr 27 10:42:41 2010 +0200 (2010-04-27) | |

changeset 36416 | 9459be72b89e |

parent 36415 | a168ac750096 |

child 36417 | 54bc1a44967d |

child 36422 | 69004340f53c |

NEWS and CONTRIBUTORS

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