src/HOL/Library/Sublist.thy
2017-01-12 blanchet 2017-01-12 added lemma
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-05-29 nipkow 2016-05-29 added subtheory of longest common prefix
2016-05-26 nipkow 2016-05-26 added function "prefixes" and some lemmas
2016-05-25 nipkow 2016-05-25 renamed suffix(eq)
2016-05-23 nipkow 2016-05-23 renamed prefix* in Library/Sublist
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-04-10 wenzelm 2015-04-10 tuned proofs;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-03 Christian Sternagel 2014-07-03 weaker assumption for "list_emb_trans"; added lemma
2014-07-03 Christian Sternagel 2014-07-03 added monotonicity lemma for list embedding
2014-07-03 Christian Sternagel 2014-07-03 no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
2014-07-03 Christian Sternagel 2014-07-03 renamed "list_hembeq" into slightly shorter "list_emb"
2014-02-19 traytel 2014-02-19 reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
2013-11-20 blanchet 2013-11-20 factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
2013-11-19 blanchet 2013-11-19 optimized more bad apples
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2012-12-13 Christian Sternagel 2012-12-13 renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS
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