# HG changeset patch # User Christian Sternagel # Date 1346731588 -32400 # Node ID 0ee5983e3d59c4eea9050327a0566ddfe599fe33 # Parent 84699f37481d8598e72202b0545e1b7ca1a3b126 NEWS; CONTRIBUTORS diff -r 84699f37481d -r 0ee5983e3d59 CONTRIBUTORS --- a/CONTRIBUTORS Wed Sep 05 13:02:25 2012 +0200 +++ b/CONTRIBUTORS Tue Sep 04 13:06:28 2012 +0900 @@ -6,6 +6,10 @@ Contributions to this Isabelle version -------------------------------------- +* September 2012: Christian Sternagel, JAIST + Consolidated HOL/Library (theories: Prefix_Order, Sublist, and + Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists. + * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM New (co)datatype package. diff -r 84699f37481d -r 0ee5983e3d59 NEWS --- a/NEWS Wed Sep 05 13:02:25 2012 +0200 +++ b/NEWS Tue Sep 04 13:06:28 2012 +0900 @@ -41,6 +41,51 @@ *** HOL *** +* Renamed theory Library/List_Prefix to Library/Sublist. +INCOMPATIBILITY. Related changes are: + + - Renamed constants: + + prefix ~> prefixeq + strict_prefix ~> prefix + + Renamed lemmas accordingly, INCOMPATIBILITY. + + - Replaced constant "postfix" by "suffixeq" with swapped argument order + (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped old infix + syntax "xs >>= ys"; use "suffixeq ys xs" instead. Renamed lemmas + accordingly. INCOMPATIBILITY. + + - New constant "emb" for homeomorphic embedding on lists. New + abbreviation "sub" for special case "emb (op =)". + + - Library/Sublist does no longer provide "order" and "bot" type class + instances for the prefix order (merely corresponding locale + interpretations). The type class instances are to be found in + Library/Prefix_Order. INCOMPATIBILITY. + + - The sublist relation from Library/Sublist_Order is now based on + "Sublist.sub". Replaced lemmas: + + le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff + le_list_append_mono ~> Sublist.emb_append_mono + le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2 + le_list_Cons_EX ~> Sublist.emb_ConsD + le_list_drop_Cons2 ~> Sublist.sub_Cons2' + le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq + le_list_drop_Cons ~> Sublist.sub_Cons' + le_list_drop_many ~> Sublist.sub_drop_many + le_list_filter_left ~> Sublist.sub_filter_left + le_list_rev_drop_many ~> Sublist.sub_rev_drop_many + le_list_rev_take_iff ~> Sublist.sub_append + le_list_same_length ~> Sublist.sub_same_length + le_list_take_many_iff ~> Sublist.sub_append' + less_eq_list.drop ~> less_eq_list_drop + less_eq_list.induct ~> less_eq_list_induct + not_le_list_length ~> Sublist.not_sub_length + + INCOMPATIBILITY. + * HOL/Codatatype: New (co)datatype package with support for mixed, nested recursion and interesting non-free datatypes.