Mon, 20 Aug 2007 20:43:59 +0200 | wenzelm | TextIO.inputLine: non-critical (assume exclusive ownership); | changeset | files |
Mon, 20 Aug 2007 20:43:58 +0200 | wenzelm | tuned merge operations via pointer_eq; | changeset | files |
Mon, 20 Aug 2007 20:38:32 +0200 | huffman | cleaned up; declared more simp rules | changeset | files |