| Tue, 11 Jul 2006 14:21:08 +0200 | wenzelm | uniform treatment of num/xnum; | changeset | files |
| Tue, 11 Jul 2006 14:21:07 +0200 | wenzelm | replaced read_radixint by read_intinf; | changeset | files |
| Tue, 11 Jul 2006 14:21:05 +0200 | wenzelm | removed str_to_int in favour of general Syntax.read_xnum; | changeset | files |
| Tue, 11 Jul 2006 14:21:04 +0200 | wenzelm | num/xnum: bin or hex; | changeset | files |
| Tue, 11 Jul 2006 12:24:23 +0200 | wenzelm | Name.internal; | changeset | files |
| Tue, 11 Jul 2006 12:22:58 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 11 Jul 2006 12:17:30 +0200 | wenzelm | * Pure: structure Name; | changeset | files |