| 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 |
| Thu, 25 Nov 2010 14:35:52 +0100 | nipkow | Added the simplest finite Ramsey theorem | file | diff | annotate |
| Sun, 24 Oct 2010 20:19:00 +0200 | nipkow | nat_number -> eval_nat_numeral | file | diff | annotate |
| Wed, 17 Feb 2010 10:30:36 -0800 | huffman | fix more looping simp rules | file | diff | annotate |
| Sat, 16 Jan 2010 17:15:28 +0100 | haftmann | dropped some old primrecs and some constdefs | file | diff | annotate |
| Sat, 17 Oct 2009 14:43:18 +0200 | wenzelm | eliminated hard tabulators, guessing at each author's individual tab-width; | file | diff | annotate |
| Fri, 27 Mar 2009 10:05:11 +0100 | haftmann | normalized imports | file | diff | annotate |
| Thu, 13 Nov 2008 15:58:38 +0100 | haftmann | simproc for let | file | diff | annotate |
| Mon, 07 Jul 2008 08:47:17 +0200 | haftmann | absolute imports of HOL/*.thy theories | file | diff | annotate |
| Thu, 26 Jun 2008 10:07:01 +0200 | haftmann | established Plain theory and image | file | diff | annotate |
| Tue, 18 Dec 2007 14:37:00 +0100 | haftmann | switched from PreList to ATP_Linkup | file | diff | annotate |
| Mon, 10 Dec 2007 11:24:09 +0100 | haftmann | switched import from Main to PreList | file | diff | annotate |
| Fri, 05 Oct 2007 08:38:09 +0200 | nipkow | added lemmas | file | diff | annotate |
| Fri, 13 Apr 2007 21:26:35 +0200 | wenzelm | tuned document (headers, sections, spacing); | file | diff | annotate |
| Tue, 27 Feb 2007 00:33:49 +0100 | wenzelm | tuned document; | file | diff | annotate |
| Mon, 04 Dec 2006 15:15:09 +0100 | krauss | fixed definition syntax | file | diff | annotate |
| Sun, 01 Oct 2006 18:29:28 +0200 | wenzelm | moved theory Infinite_Set to Library; | file | diff | annotate |
| Wed, 28 Jun 2006 09:27:53 +0200 | paulson | disjunctive wellfoundedness | file | diff | annotate |
| Sat, 24 Jun 2006 22:54:37 +0200 | wenzelm | fix/fixes: tuned type constraints; | file | diff | annotate |
| Sat, 24 Jun 2006 22:25:31 +0200 | wenzelm | minor tuning of definitions/proofs; | file | diff | annotate |
| Fri, 23 Jun 2006 13:42:19 +0200 | nipkow | beautification | file | diff | annotate |
| Fri, 23 Jun 2006 09:55:01 +0200 | paulson | Introduction of Ramsey's theorem | file | diff | annotate |