Sat, 29 May 2004 15:02:35 +0200 | wenzelm | Output.add_mode; Output.timing; | changeset | files |
Sat, 29 May 2004 15:02:13 +0200 | wenzelm | output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT; | changeset | files |
Sat, 29 May 2004 15:01:36 +0200 | wenzelm | Output.timing; | changeset | files |