| Thu, 10 Jan 2008 19:09:21 +0100 |
berghofe |
New interface for test data generators.
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:16:01 +0100 |
paulson |
comment
|
file |
diff |
annotate
|
| Mon, 22 Oct 2007 16:54:50 +0200 |
haftmann |
dropped superfluous inlining lemmas
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 07:48:23 +0200 |
haftmann |
dropped doubled proof
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 11:53:17 +0200 |
berghofe |
Generalized code generator for numerals.
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 20:52:18 +0200 |
huffman |
replace iszero_number_of_Pls with iszero_0 in rel_simps
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:42 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:49 +0200 |
haftmann |
clarified import
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:11 +0200 |
wenzelm |
added Tools/numeral.ML;
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 05:20:05 +0200 |
huffman |
modify proofs to avoid referring to int::nat=>int
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:48:35 +0200 |
berghofe |
Adapted to new syntax for case expressions.
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Mon, 12 Aug 2002 17:48:15 +0200 |
nipkow |
Added Mi and Max on sets, hid Min and Pls on numerals.
|
file |
diff |
annotate
|
| Sun, 13 Jan 2002 21:13:59 +0100 |
wenzelm |
symbolic syntax for x^2 (faills back on plain infix "^");
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Thu, 08 Nov 2001 00:25:36 +0100 |
wenzelm |
use num_const of Pure;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:49:59 +0200 |
wenzelm |
"num" syntax;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2001 17:38:29 +0200 |
wenzelm |
constify numeral tokens in order to allow translations;
|
file |
diff |
annotate
|
| Sun, 23 Jul 2000 12:02:22 +0200 |
wenzelm |
removed selector syntax -- improper tuples are broken beyond repair :-(
|
file |
diff |
annotate
|