src/Pure/Thy/symbol_input.ML
1996-12-16 wenzelm 1996-12-16 symbol_input.ML: Defines 'use' command with symbol input filtering.