Mon, 17 Apr 2000 14:06:05 +0200 | wenzelm | added 'hide'; | changeset | files |
Mon, 17 Apr 2000 14:04:46 +0200 | wenzelm | tuned msg; | changeset | files |
Mon, 17 Apr 2000 14:03:51 +0200 | wenzelm | NameSpace.is_qualified; | changeset | files |
Mon, 17 Apr 2000 13:57:55 +0200 | wenzelm | Pretty.chunks; | changeset | files |
Sat, 15 Apr 2000 17:41:20 +0200 | nipkow | mod to error msg | changeset | files |
Sat, 15 Apr 2000 15:01:31 +0200 | wenzelm | next_block: reset_facts; | changeset | files |