removed Pure/Syntax/ROOT.ML;
authorwenzelm
Sat Apr 14 17:36:06 2007 +0200 (2007-04-14)
changeset 2267968cd69a388e2
parent 22678 23963361278c
child 22680 31a2303f4283
removed Pure/Syntax/ROOT.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/Syntax/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Sat Apr 14 17:36:05 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sat Apr 14 17:36:06 2007 +0200
     1.3 @@ -52,24 +52,23 @@
     1.4    ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_tests.ML	\
     1.5    ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML			\
     1.6    ProofGeneral/proof_general_pgip.ML ProofGeneral/proof_general_emacs.ML	\
     1.7 -  ProofGeneral/ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML 		\
     1.8 -  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML		\
     1.9 -  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML		\
    1.10 -  Thy/latex.ML Thy/ml_context.ML Thy/present.ML Thy/term_style.ML		\
    1.11 -  Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML		\
    1.12 -  Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML Tools/am_compiler.ML		\
    1.13 -  Tools/am_interpreter.ML Tools/am_util.ML Tools/class_package.ML		\
    1.14 -  Tools/codegen_consts.ML Tools/codegen_data.ML Tools/codegen_func.ML		\
    1.15 -  Tools/codegen_funcgr.ML Tools/codegen_names.ML Tools/codegen_package.ML	\
    1.16 -  Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/compute.ML		\
    1.17 -  Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
    1.18 -  Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML compress.ML		\
    1.19 -  conjunction.ML consts.ML context.ML defs.ML display.ML drule.ML envir.ML	\
    1.20 -  fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML 	\
    1.21 -  more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML   \
    1.22 -  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML     \
    1.23 -  tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML       \
    1.24 -  unify.ML variable.ML
    1.25 +  ProofGeneral/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML		\
    1.26 +  Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML	\
    1.27 +  Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML Thy/latex.ML 			\
    1.28 +  Thy/ml_context.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML	\
    1.29 +  Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML		\
    1.30 +  Thy/thy_output.ML Tools/ROOT.ML Tools/am_compiler.ML Tools/am_interpreter.ML	\
    1.31 +  Tools/am_util.ML Tools/class_package.ML Tools/codegen_consts.ML		\
    1.32 +  Tools/codegen_data.ML Tools/codegen_func.ML Tools/codegen_funcgr.ML		\
    1.33 +  Tools/codegen_names.ML Tools/codegen_package.ML Tools/codegen_serializer.ML	\
    1.34 +  Tools/codegen_thingol.ML Tools/compute.ML Tools/invoke.ML Tools/nbe.ML 	\
    1.35 +  Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml_syntax.ML assumption.ML	\
    1.36 +  axclass.ML codegen.ML compress.ML conjunction.ML consts.ML context.ML defs.ML	\
    1.37 +  display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML 	\
    1.38 +  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML		\
    1.39 +  old_goals.ML pattern.ML proofterm.ML pure_thy.ML search.ML sign.ML		\
    1.40 +  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML	\
    1.41 +  theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
    1.42  	@./mk
    1.43  
    1.44  
     2.1 --- a/src/Pure/ROOT.ML	Sat Apr 14 17:36:05 2007 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sat Apr 14 17:36:06 2007 +0200
     2.3 @@ -9,9 +9,6 @@
     2.4  
     2.5  print_depth 10;
     2.6  
     2.7 -(*fake hiding of private structures*)
     2.8 -structure Hidden = struct end;
     2.9 -
    2.10  (*basic tools*)
    2.11  use "General/basics.ML";
    2.12  use "library.ML";
    2.13 @@ -34,13 +31,31 @@
    2.14  use "compress.ML";
    2.15  
    2.16  (*inner syntax module*)
    2.17 -cd "Syntax"; use "ROOT.ML"; cd "..";
    2.18 +use "Syntax/lexicon.ML";
    2.19 +use "Syntax/ast.ML";
    2.20 +use "Syntax/syn_ext.ML";
    2.21 +use "Syntax/parser.ML";
    2.22 +use "Syntax/type_ext.ML";
    2.23 +use "Syntax/syn_trans.ML";
    2.24 +use "Syntax/mixfix.ML";
    2.25 +use "Syntax/printer.ML";
    2.26 +use "Syntax/syntax.ML";
    2.27 +structure Hidden = struct end;
    2.28 +structure Lexicon = Hidden;
    2.29 +structure Ast = Hidden;
    2.30 +structure SynExt = Hidden;
    2.31 +structure Parser = Hidden;
    2.32 +structure TypeExt = Hidden;
    2.33 +structure SynTrans = Hidden;
    2.34 +structure Mixfix = Hidden;
    2.35 +structure Printer = Hidden;
    2.36 +
    2.37 +use "type_infer.ML";
    2.38  use "General/ml_syntax.ML";
    2.39  
    2.40  (*core of tactical proof system*)
    2.41  use "envir.ML";
    2.42  use "logic.ML";
    2.43 -use "type_infer.ML";
    2.44  use "consts.ML";
    2.45  use "sign.ML";
    2.46  use "pattern.ML";
     3.1 --- a/src/Pure/Syntax/ROOT.ML	Sat Apr 14 17:36:05 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,26 +0,0 @@
     3.4 -(*  Title:      Pure/Syntax/ROOT.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3.7 -
     3.8 -This file builds the syntax module.
     3.9 -*)
    3.10 -
    3.11 -use "lexicon.ML";
    3.12 -use "ast.ML";
    3.13 -use "syn_ext.ML";
    3.14 -use "parser.ML";
    3.15 -use "type_ext.ML";
    3.16 -use "syn_trans.ML";
    3.17 -use "mixfix.ML";
    3.18 -use "printer.ML";
    3.19 -use "syntax.ML";
    3.20 -
    3.21 -(*hiding private stuff*)
    3.22 -structure Lexicon = Hidden;
    3.23 -structure Ast = Hidden;
    3.24 -structure SynExt = Hidden;
    3.25 -structure Parser = Hidden;
    3.26 -structure TypeExt = Hidden;
    3.27 -structure SynTrans = Hidden;
    3.28 -structure Mixfix = Hidden;
    3.29 -structure Printer = Hidden;