NEWS
changeset 50516 ed6b40d15d1c
parent 50455 c7f366a861ed
child 50524 bd145273e7c6
     1.1 --- a/NEWS	Thu Dec 13 09:21:45 2012 +0100
     1.2 +++ b/NEWS	Thu Dec 13 13:11:38 2012 +0100
     1.3 @@ -173,8 +173,8 @@
     1.4      syntax "xs >>= ys"; use "suffixeq ys xs" instead.  Renamed lemmas
     1.5      accordingly.  INCOMPATIBILITY.
     1.6  
     1.7 -  - New constant "emb" for homeomorphic embedding on lists. New
     1.8 -    abbreviation "sub" for special case "emb (op =)".
     1.9 +  - New constant "list_hembeq" for homeomorphic embedding on lists. New
    1.10 +    abbreviation "sublisteq" for special case "list_hembeq (op =)".
    1.11  
    1.12    - Library/Sublist does no longer provide "order" and "bot" type class
    1.13      instances for the prefix order (merely corresponding locale
    1.14 @@ -182,24 +182,24 @@
    1.15      Library/Prefix_Order. INCOMPATIBILITY.
    1.16  
    1.17    - The sublist relation from Library/Sublist_Order is now based on
    1.18 -    "Sublist.sub". Replaced lemmas:
    1.19 -
    1.20 -      le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
    1.21 -      le_list_append_mono ~> Sublist.emb_append_mono
    1.22 -      le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
    1.23 -      le_list_Cons_EX ~> Sublist.emb_ConsD
    1.24 -      le_list_drop_Cons2 ~> Sublist.sub_Cons2'
    1.25 -      le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
    1.26 -      le_list_drop_Cons ~> Sublist.sub_Cons'
    1.27 -      le_list_drop_many ~> Sublist.sub_drop_many
    1.28 -      le_list_filter_left ~> Sublist.sub_filter_left
    1.29 -      le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
    1.30 -      le_list_rev_take_iff ~> Sublist.sub_append
    1.31 -      le_list_same_length ~> Sublist.sub_same_length
    1.32 -      le_list_take_many_iff ~> Sublist.sub_append'
    1.33 +    "Sublist.sublisteq". Replaced lemmas:
    1.34 +
    1.35 +      le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
    1.36 +      le_list_append_mono ~> Sublist.list_hembeq_append_mono
    1.37 +      le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
    1.38 +      le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
    1.39 +      le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
    1.40 +      le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
    1.41 +      le_list_drop_Cons ~> Sublist.sublisteq_Cons'
    1.42 +      le_list_drop_many ~> Sublist.sublisteq_drop_many
    1.43 +      le_list_filter_left ~> Sublist.sublisteq_filter_left
    1.44 +      le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
    1.45 +      le_list_rev_take_iff ~> Sublist.sublisteq_append
    1.46 +      le_list_same_length ~> Sublist.sublisteq_same_length
    1.47 +      le_list_take_many_iff ~> Sublist.sublisteq_append'
    1.48        less_eq_list.drop ~> less_eq_list_drop
    1.49        less_eq_list.induct ~> less_eq_list_induct
    1.50 -      not_le_list_length ~> Sublist.not_sub_length
    1.51 +      not_le_list_length ~> Sublist.not_sublisteq_length
    1.52  
    1.53      INCOMPATIBILITY.
    1.54