--- a/NEWS Thu Dec 13 09:21:45 2012 +0100
+++ b/NEWS Thu Dec 13 13:11:38 2012 +0100
@@ -173,8 +173,8 @@
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 =)".
+ - New constant "list_hembeq" for homeomorphic embedding on lists. New
+ abbreviation "sublisteq" for special case "list_hembeq (op =)".
- Library/Sublist does no longer provide "order" and "bot" type class
instances for the prefix order (merely corresponding locale
@@ -182,24 +182,24 @@
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'
+ "Sublist.sublisteq". Replaced lemmas:
+
+ le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff
+ le_list_append_mono ~> Sublist.list_hembeq_append_mono
+ le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2
+ le_list_Cons_EX ~> Sublist.list_hembeq_ConsD
+ le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'
+ le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq
+ le_list_drop_Cons ~> Sublist.sublisteq_Cons'
+ le_list_drop_many ~> Sublist.sublisteq_drop_many
+ le_list_filter_left ~> Sublist.sublisteq_filter_left
+ le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many
+ le_list_rev_take_iff ~> Sublist.sublisteq_append
+ le_list_same_length ~> Sublist.sublisteq_same_length
+ le_list_take_many_iff ~> Sublist.sublisteq_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
+ not_le_list_length ~> Sublist.not_sublisteq_length
INCOMPATIBILITY.