NEWS; CONTRIBUTORS
authorChristian Sternagel
Tue Sep 04 13:06:28 2012 +0900 (2012-09-04)
changeset 491450ee5983e3d59
parent 49144 84699f37481d
child 49154 4c507e92e4a2
NEWS; CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Wed Sep 05 13:02:25 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Sep 04 13:06:28 2012 +0900
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* September 2012: Christian Sternagel, JAIST
     1.8 +  Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
     1.9 +  Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
    1.10 +
    1.11  * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
    1.12    New (co)datatype package.
    1.13  
     2.1 --- a/NEWS	Wed Sep 05 13:02:25 2012 +0200
     2.2 +++ b/NEWS	Tue Sep 04 13:06:28 2012 +0900
     2.3 @@ -41,6 +41,51 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Renamed theory Library/List_Prefix to Library/Sublist.
     2.8 +INCOMPATIBILITY.  Related changes are:
     2.9 +
    2.10 +  - Renamed constants:
    2.11 +
    2.12 +      prefix ~> prefixeq
    2.13 +      strict_prefix ~> prefix
    2.14 +
    2.15 +    Renamed lemmas accordingly, INCOMPATIBILITY.
    2.16 +
    2.17 +  - Replaced constant "postfix" by "suffixeq" with swapped argument order
    2.18 +    (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped old infix
    2.19 +    syntax "xs >>= ys"; use "suffixeq ys xs" instead.  Renamed lemmas
    2.20 +    accordingly.  INCOMPATIBILITY.
    2.21 +
    2.22 +  - New constant "emb" for homeomorphic embedding on lists. New
    2.23 +    abbreviation "sub" for special case "emb (op =)".
    2.24 +
    2.25 +  - Library/Sublist does no longer provide "order" and "bot" type class
    2.26 +    instances for the prefix order (merely corresponding locale
    2.27 +    interpretations). The type class instances are to be found in
    2.28 +    Library/Prefix_Order. INCOMPATIBILITY.
    2.29 +
    2.30 +  - The sublist relation from Library/Sublist_Order is now based on
    2.31 +    "Sublist.sub". Replaced lemmas:
    2.32 +
    2.33 +      le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
    2.34 +      le_list_append_mono ~> Sublist.emb_append_mono
    2.35 +      le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
    2.36 +      le_list_Cons_EX ~> Sublist.emb_ConsD
    2.37 +      le_list_drop_Cons2 ~> Sublist.sub_Cons2'
    2.38 +      le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
    2.39 +      le_list_drop_Cons ~> Sublist.sub_Cons'
    2.40 +      le_list_drop_many ~> Sublist.sub_drop_many
    2.41 +      le_list_filter_left ~> Sublist.sub_filter_left
    2.42 +      le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
    2.43 +      le_list_rev_take_iff ~> Sublist.sub_append
    2.44 +      le_list_same_length ~> Sublist.sub_same_length
    2.45 +      le_list_take_many_iff ~> Sublist.sub_append'
    2.46 +      less_eq_list.drop ~> less_eq_list_drop
    2.47 +      less_eq_list.induct ~> less_eq_list_induct
    2.48 +      not_le_list_length ~> Sublist.not_sub_length
    2.49 +
    2.50 +    INCOMPATIBILITY.
    2.51 +
    2.52  * HOL/Codatatype: New (co)datatype package with support for mixed,
    2.53  nested recursion and interesting non-free datatypes.
    2.54