| 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
|
| Sun, 16 Jul 2000 20:51:19 +0200 |
wenzelm |
added syntax for proper / improper selector functions;
|
file |
diff |
annotate
|
| Sun, 04 Jun 2000 19:39:29 +0200 |
wenzelm |
removed explicit terminator (";");
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:42:31 +0200 |
paulson |
renamed sort "numeral" to "number"
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:08:30 +0200 |
wenzelm |
added Numeral.thy, Tools/numeral_syntax.ML;
|
file |
diff |
annotate
|