added symbol_font.ML;
authorwenzelm
Mon, 18 Nov 1996 17:29:05 +0100
changeset 2198 0dddd9575717
parent 2197 e895937fcd56
child 2199 bcb360f80dac
added symbol_font.ML;
src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Mon Nov 18 17:28:40 1996 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Mon Nov 18 17:29:05 1996 +0100
@@ -5,6 +5,7 @@
 This file builds the syntax module.
 *)
 
+use "symbol_font.ML";
 use "pretty.ML";
 use "lexicon.ML";
 use "ast.ML";