| Mon, 23 Oct 2017 14:45:10 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sat, 21 Oct 2017 18:19:11 +0200 |
bulwahn |
remove trailing whitespaces in List
|
file |
diff |
annotate
|
| Sat, 21 Oct 2017 18:16:56 +0200 |
bulwahn |
drop a superfluous assumption that was found by the find_unused_assms command
|
file |
diff |
annotate
|
| Sat, 21 Oct 2017 18:14:59 +0200 |
bulwahn |
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
|
file |
diff |
annotate
|
| Sat, 21 Oct 2017 18:11:29 +0200 |
bulwahn |
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
|
file |
diff |
annotate
|
| Mon, 16 Oct 2017 08:00:28 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Fri, 13 Oct 2017 09:01:27 +0200 |
nipkow |
added lemmas, tuned spaces
|
file |
diff |
annotate
|
| Thu, 12 Oct 2017 05:37:58 +0200 |
nipkow |
relaxed assm
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:47 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Thu, 14 Sep 2017 19:21:32 +0200 |
nipkow |
two new simp rules
|
file |
diff |
annotate
|
| Thu, 14 Sep 2017 17:36:06 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 13 Sep 2017 17:40:54 +0200 |
nipkow |
added lemma; zip_with -> map2
|
file |
diff |
annotate
|
| Tue, 12 Sep 2017 20:40:46 +0200 |
nipkow |
introduced zip_with
|
file |
diff |
annotate
|
| Tue, 12 Sep 2017 12:14:38 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 09:45:56 +0200 |
bulwahn |
more facts on Map.map_of and List.zip
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 16:24:14 +0200 |
eberlm |
Some small lemmas about polynomials and FPSs
|
file |
diff |
annotate
|
| Fri, 25 Aug 2017 08:59:54 +0200 |
nipkow |
Added lemmas
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 07:27:17 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 16 Aug 2017 21:14:11 +0200 |
nipkow |
more reorganization around sorted_wrt
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 19:47:08 +0200 |
nipkow |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
file |
diff |
annotate
|
| Sun, 06 Aug 2017 21:49:25 +0200 |
bulwahn |
slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned
|
file |
diff |
annotate
|
| Sat, 08 Jul 2017 17:33:11 +0200 |
nipkow |
revised lemma
|
file |
diff |
annotate
|
| Sat, 08 Jul 2017 15:51:29 +0200 |
nipkow |
generalized lemma
|
file |
diff |
annotate
|
| Fri, 07 Jul 2017 11:32:06 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Mon, 29 May 2017 09:14:15 +0200 |
eberlm |
reorganised material on sublists
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 16:56:45 +0200 |
eberlm |
added shuffle product to HOL/List
|
file |
diff |
annotate
|
| Sun, 29 Jan 2017 17:27:02 +0100 |
wenzelm |
added inj_def (redundant, analogous to surj_def, bij_def);
|
file |
diff |
annotate
|
| Sun, 29 Jan 2017 13:28:45 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 12 Jan 2017 15:54:13 +0100 |
blanchet |
added lemma
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 21:28:09 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 00:14:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2016 11:02:23 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 18:57:20 +0200 |
haftmann |
lists form a monoid
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2016 14:09:55 +0200 |
Lars Hupel |
added missing transfer rule
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 17:57:09 +0200 |
eberlm |
Various additions to polynomials, FPSs, Gamma function
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:10:48 +0200 |
nipkow |
added subtheory of longest common prefix
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:33:01 +0100 |
haftmann |
moved
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 11:39:26 +0100 |
traytel |
call the predicator of list list_all
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 23:07:06 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 16:37:56 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 16:36:41 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 05 Jan 2016 17:54:10 +0100 |
eberlm |
Added some facts about polynomials
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 17:16:21 +0100 |
wenzelm |
discontinued ASCII replacement syntax <->;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2015 15:23:34 +0000 |
paulson |
New theorems mostly from Peter Gammie
|
file |
diff |
annotate
|