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