src/HOL/Library/Sublist.thy
Fri, 05 Mar 2021 15:01:59 +0100 desharna added lemmas (sublist|prefix|suffix)_list_all
Fri, 05 Mar 2021 14:23:14 +0100 desharna added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
Sat, 30 Jan 2021 07:31:06 +0100 nipkow Simpler proof
Thu, 23 Apr 2020 09:57:41 +0200 nipkow added lemmas
Thu, 07 Jun 2018 19:36:12 +0200 nipkow utilize 'flip'
Thu, 15 Feb 2018 13:04:36 +0100 wenzelm merged
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Wed, 14 Feb 2018 16:32:09 +0100 nipkow New theory ex/Radix_Sort.thy
Mon, 12 Feb 2018 20:17:53 +0100 nipkow added lemmas
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 29 May 2017 16:40:56 +0200 eberlm Tuned Library/Sublist.thy
Mon, 29 May 2017 09:14:15 +0200 eberlm reorganised material on sublists
Sun, 28 May 2017 13:57:43 +0200 nipkow introduced arg_max
Thu, 18 May 2017 12:02:21 +0200 eberlm more on sublists
Thu, 12 Jan 2017 15:54:13 +0100 blanchet added lemma
Wed, 10 Aug 2016 14:50:59 +0200 wenzelm tuned proofs;
Sun, 29 May 2016 14:10:48 +0200 nipkow added subtheory of longest common prefix
Thu, 26 May 2016 09:05:00 +0200 nipkow added function "prefixes" and some lemmas
Wed, 25 May 2016 17:40:56 +0200 nipkow renamed suffix(eq)
Mon, 23 May 2016 22:43:11 +0200 nipkow renamed prefix* in Library/Sublist
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Fri, 10 Apr 2015 11:52:55 +0200 wenzelm tuned proofs;
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Thu, 03 Jul 2014 09:55:16 +0200 Christian Sternagel weaker assumption for "list_emb_trans"; added lemma
Thu, 03 Jul 2014 09:55:15 +0200 Christian Sternagel added monotonicity lemma for list embedding
Thu, 03 Jul 2014 09:55:15 +0200 Christian Sternagel no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
Thu, 03 Jul 2014 09:55:15 +0200 Christian Sternagel renamed "list_hembeq" into slightly shorter "list_emb"
Wed, 19 Feb 2014 10:30:21 +0100 traytel reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
Wed, 20 Nov 2013 18:58:00 +0100 blanchet factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
Tue, 19 Nov 2013 01:29:50 +0100 blanchet optimized more bad apples
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Thu, 13 Dec 2012 13:11:38 +0100 Christian Sternagel renamed "emb" to "list_hembeq";
Mon, 03 Sep 2012 23:03:54 +0200 wenzelm misc tuning;
Thu, 30 Aug 2012 13:03:03 +0900 Christian Sternagel List is implicitly imported by Main
Wed, 29 Aug 2012 16:25:35 +0900 Christian Sternagel introduced "sub" as abbreviation for "emb (op =)";
Wed, 29 Aug 2012 11:05:44 +0900 Christian Sternagel more lemmas on suffixes and embedding
Wed, 29 Aug 2012 10:57:24 +0900 Christian Sternagel changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
Thu, 30 Aug 2012 13:05:11 +0900 Christian Sternagel added author
Wed, 29 Aug 2012 12:23:14 +0900 Christian Sternagel dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
Wed, 29 Aug 2012 10:48:28 +0900 Christian Sternagel added embedding for lists (constant emb)
Wed, 29 Aug 2012 10:46:11 +0900 Christian Sternagel renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=
Wed, 29 Aug 2012 10:35:05 +0900 Christian Sternagel renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix
Wed, 29 Aug 2012 10:27:56 +0900 Christian Sternagel renamed theory List_Prefix into Sublist (since it is not only about prefixes)
Sat, 19 Jul 2008 19:27:13 +0200 bulwahn added verification framework for the HeapMonad and quicksort as example for this framework
less more (0) tip