src/Pure/Thy/symbol_input.ML
Wed, 06 Aug 1997 00:29:02 +0200 berghofe Removed function file_exists (now included in library.ML)
Mon, 16 Dec 1996 10:02:48 +0100 wenzelm symbol_input.ML: Defines 'use' command with symbol input filtering.
less more (0) tip