src/Pure/General/symbol.ML
Fri, 21 May 1999 16:22:39 +0200 wenzelm avoid string constants;
Wed, 12 May 1999 16:52:28 +0200 wenzelm rearranged order of modules;
Tue, 09 Mar 1999 12:10:13 +0100 wenzelm tuned using nth_elem_string, exists_string;
Thu, 11 Feb 1999 21:16:30 +0100 wenzelm added output_width;
Thu, 04 Feb 1999 18:14:40 +0100 wenzelm added 'use';
Fri, 29 Jan 1999 17:12:14 +0100 oheimb renamed space2 to spacespace
Wed, 13 Jan 1999 15:18:02 +0100 wenzelm fixed titles;
Wed, 13 Jan 1999 12:44:33 +0100 wenzelm files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
less more (0) tip