| Tue, 27 Feb 2024 14:57:36 +0000 |
paulson |
Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers
|
file |
diff |
annotate
|
| Sun, 11 Feb 2024 12:52:14 +0000 |
paulson |
new lemmas involving Ramsey numbers, infinite sets
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 18:30:18 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Wed, 19 May 2021 14:17:40 +0100 |
paulson |
things need to be ugly
|
file |
diff |
annotate
|
| Mon, 10 May 2021 16:14:34 +0200 |
wenzelm |
tuned proofs --- avoid z3, which is absent on arm64-linux;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2020 17:18:47 +0100 |
paulson |
a new lemma
|
file |
diff |
annotate
|
| Wed, 20 May 2020 15:00:25 +0100 |
paulson |
A few new theorems, plus some tidying up
|
file |
diff |
annotate
|
| Wed, 26 Feb 2020 12:21:48 +0000 |
paulson |
Moved a number of general-purpose lemmas into HOL
|
file |
diff |
annotate
|
| Mon, 24 Feb 2020 12:14:13 +0000 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Mon, 17 Feb 2020 11:07:27 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
| Mon, 17 Feb 2020 11:07:09 +0000 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Sun, 16 Feb 2020 18:01:03 +0100 |
nipkow |
lemmas about "card A = 2"; prefer iff to implications
|
file |
diff |
annotate
|
| Mon, 27 Jan 2020 14:58:17 +0000 |
paulson |
Two lemmas about nsets
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 16:37:26 +0000 |
paulson |
corrected some confusing terminology / notation
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 16:13:36 +0000 |
paulson |
Ramsey with multiple colours and arbitrary exponents
|
file |
diff |
annotate
|
| Fri, 08 Nov 2019 16:07:22 +0000 |
paulson |
A slight tidying up of messy proof steps
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 01 Mar 2017 17:09:54 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:44:31 +0200 |
wenzelm |
some uses of 'obtain' with structure statement;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 22:29:12 +0200 |
wenzelm |
tuned proofs -- slightly faster;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 23:12:08 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 12:27:03 +0100 |
traytel |
adapt to 9733ab5c1df6
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 16:48:10 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|