# 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.