Mon, 09 Jun 2025 22:14:38 +0200 |
haftmann |
more qualified auxiliary operations
|
file |
diff |
annotate
|
Fri, 21 Mar 2025 10:45:56 +0000 |
paulson |
New theorems, mostly from the number theory project
|
file |
diff |
annotate
|
Fri, 28 Feb 2025 13:50:18 +0000 |
paulson |
Some new lemmas and some tidying
|
file |
diff |
annotate
|
Sun, 03 Nov 2024 22:29:07 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
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
|