NEWS

   - 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 =)".
+  - 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
     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'
+    "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.
 
 * HOL/Rings: renamed lemmas