| Mon, 27 Oct 1997 15:43:53 +0100 | wenzelm | flipped global_names default; | changeset | files |
| Mon, 27 Oct 1997 15:43:16 +0100 | wenzelm | do not change global_names flag; | changeset | files |
| Mon, 27 Oct 1997 15:29:01 +0100 | wenzelm | Isa94-2 instead of Isa95; | changeset | files |