added Syntax/symbol_font.ML;
authorwenzelm
Mon Nov 18 17:27:59 1996 +0100 (1996-11-18)
changeset 2195e8271379ba4b
parent 2194 63a68a3a8a76
child 2196 1b36ebc70487
added Syntax/symbol_font.ML;
src/Pure/Makefile
     1.1 --- a/src/Pure/Makefile	Mon Nov 18 16:34:37 1996 +0100
     1.2 +++ b/src/Pure/Makefile	Mon Nov 18 17:27:59 1996 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  SYNTAX_FILES =	Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
     1.5  	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/syn_trans.ML\
     1.6  	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
     1.7 -	Syntax/syn_ext.ML	Syntax/mixfix.ML
     1.8 +	Syntax/syn_ext.ML	Syntax/mixfix.ML	Syntax/symbol_font.ML
     1.9  
    1.10  THY_FILES = Thy/ROOT.ML		Thy/thy_scan.ML		Thy/thy_parse.ML\
    1.11  	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML