# HG changeset patch # User wenzelm # Date 895590904 -7200 # Node ID a6e71e5a1004e68f43c7a29a894724c1c8a3cce8 # Parent a1b5d156ec33ce3ca5d93192a9211cadc534f434 added Thy/position.ML; diff -r a1b5d156ec33 -r a6e71e5a1004 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue May 19 17:14:28 1998 +0200 +++ b/src/Pure/IsaMakefile Tue May 19 17:15:04 1998 +0200 @@ -30,13 +30,13 @@ 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 \ - attribute.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 + Thy/path.ML Thy/position.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 attribute.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 diff -r a1b5d156ec33 -r a6e71e5a1004 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Tue May 19 17:14:28 1998 +0200 +++ b/src/Pure/Thy/ROOT.ML Tue May 19 17:15:04 1998 +0200 @@ -4,6 +4,7 @@ This file builds the theory parser and autoloading system. *) +use "position.ML"; use "path.ML"; use "file.ML"; use "use.ML";