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