src/HOL/Library/Sublist.thy
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