# HG changeset patch # User wenzelm # Date 889456006 -3600 # Node ID 033566671199c568024f43179558a7e9a6d6b5aa # Parent 8cec457a8961169f838c56cdc4cfe304cae5da16 replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; added Pure/Syntax/scan.ML; diff -r 8cec457a8961 -r 033566671199 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Mar 09 16:05:34 1998 +0100 +++ b/src/Pure/IsaMakefile Mon Mar 09 16:06:46 1998 +0100 @@ -26,15 +26,15 @@ $(OUT)/Pure: ML-Systems/mlworks.ML ML-Systems/polyml.ML \ ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \ Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ - Syntax/pretty.ML Syntax/printer.ML Syntax/symbol_font.ML \ + Syntax/pretty.ML Syntax/printer.ML Syntax/scan.ML Syntax/symbol.ML \ Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \ Thy/browser_info.ML Thy/context.ML Thy/file.ML Thy/path.ML \ Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML \ - Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML \ - display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \ - logic.ML name_space.ML net.ML pattern.ML pure_thy.ML search.ML \ - section_utils.ML seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML \ + Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML \ + deriv.ML display.ML drule.ML envir.ML goals.ML install_pp.ML \ + library.ML logic.ML name_space.ML net.ML pattern.ML pure_thy.ML \ + search.ML seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML \ term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML @./mk