| Tue, 07 May 2002 14:28:34 +0200 |
wenzelm |
be liberal about missing types;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Wed, 08 Aug 2001 17:38:29 +0200 |
wenzelm |
constify numeral tokens in order to allow translations;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2001 20:03:26 +0100 |
wenzelm |
hide dest_bin;
|
file |
diff |
annotate
|
| Mon, 18 Dec 2000 14:59:05 +0100 |
nipkow |
moved mk_bin from Numerals to HOLogic
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:11:38 +0200 |
wenzelm |
use Syntax.read_xnum;
|
file |
diff |
annotate
|
| Sat, 01 Jul 2000 19:55:22 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 14:14:14 +0200 |
nipkow |
moved inf_of(?) to hologic.
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:26:26 +0200 |
wenzelm |
observe show_types;
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:30:27 +0200 |
paulson |
now using correctly-typed constants from HOLogic
|
file |
diff |
annotate
|
| Wed, 21 Jul 1999 15:18:36 +0200 |
paulson |
now exports mk_bin
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:08:30 +0200 |
wenzelm |
added Numeral.thy, Tools/numeral_syntax.ML;
|
file |
diff |
annotate
|