Thu, 14 Jul 2005 19:28:38 +0200 | wenzelm | replaced itlist by fold_rev; | changeset | files |
Thu, 14 Jul 2005 19:28:37 +0200 | wenzelm | replaced itlist by fold_rev; | changeset | files |
Thu, 14 Jul 2005 19:28:36 +0200 | wenzelm | use sys_error instead of exception Internal; | changeset | files |
Thu, 14 Jul 2005 19:28:34 +0200 | wenzelm | sys_error; | changeset | files |