| Wed, 23 Mar 2005 12:09:18 +0100 |
paulson |
replaced bool by a new datatype "bit" for binary numerals
|
file |
diff |
annotate
|
| Tue, 08 Mar 2005 16:02:52 +0100 |
obua |
fix integer overflow in numeral syntax for SML NJ.
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Tue, 13 Aug 2002 12:16:14 +0200 |
wenzelm |
more robust printing of numerals;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2002 17:48:19 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 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
|