| 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
|