src/HOL/Library/Sublist.thy
2012-09-03 wenzelm 2012-09-03 misc tuning;
2012-08-30 Christian Sternagel 2012-08-30 List is implicitly imported by Main
2012-08-29 Christian Sternagel 2012-08-29 introduced "sub" as abbreviation for "emb (op =)"; Sublist_Order is now based on Sublist.sub; simplified and moved most lemmas on sub from Sublist_Order to Sublist; Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order
2012-08-29 Christian Sternagel 2012-08-29 more lemmas on suffixes and embedding
2012-08-29 Christian Sternagel 2012-08-29 changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
2012-08-30 Christian Sternagel 2012-08-30 added author
2012-08-29 Christian Sternagel 2012-08-29 dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
2012-08-29 Christian Sternagel 2012-08-29 added embedding for lists (constant emb)
2012-08-29 Christian Sternagel 2012-08-29 renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=
2012-08-29 Christian Sternagel 2012-08-29 renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix
2012-08-29 Christian Sternagel 2012-08-29 renamed theory List_Prefix into Sublist (since it is not only about prefixes)
2008-07-19 bulwahn 2008-07-19 added verification framework for the HeapMonad and quicksort as example for this framework