Thu, 01 Feb 2001 18:13:06 +0100 | oheimb | debugged declare | changeset | files |
Thu, 01 Feb 2001 17:03:19 +0100 | oheimb | further minor improvements | changeset | files |
Wed, 31 Jan 2001 22:16:22 +0100 | wenzelm | strip_blanks moved to General/symbol.ML; | changeset | files |
Wed, 31 Jan 2001 22:15:53 +0100 | wenzelm | pretty_text: tweak_lines handles linebreaks gracefully; | changeset | files |
Wed, 31 Jan 2001 22:14:53 +0100 | wenzelm | added strip_blanks; | changeset | files |
Wed, 31 Jan 2001 16:35:46 +0100 | oheimb | added attribute declarations, etc. | changeset | files |