added context_position.ML;
authorwenzelm
Mon Sep 29 14:41:22 2008 +0200 (2008-09-29)
changeset 28404b906dd1de855
parent 28403 da9ae7774513
child 28405 000dee6d5d80
added context_position.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Sep 29 12:32:00 2008 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Sep 29 14:41:22 2008 +0200
     1.3 @@ -76,13 +76,14 @@
     1.4    Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/quickcheck.ML	\
     1.5    Tools/value.ML Tools/isabelle_process.ML Tools/named_thms.ML		\
     1.6    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
     1.7 -  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
     1.8 -  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
     1.9 -  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    1.10 -  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML	\
    1.11 -  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
    1.12 -  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML	\
    1.13 -  type_infer.ML unify.ML variable.ML
    1.14 +  conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
    1.15 +  defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
    1.16 +  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
    1.17 +  morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML	\
    1.18 +  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
    1.19 +  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
    1.20 +  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML		\
    1.21 +  variable.ML
    1.22  	@./mk
    1.23  
    1.24  
     2.1 --- a/src/Pure/ROOT.ML	Mon Sep 29 12:32:00 2008 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Mon Sep 29 14:41:22 2008 +0200
     2.3 @@ -29,9 +29,10 @@
     2.4  use "term_subst.ML";
     2.5  use "logic.ML";
     2.6  use "General/pretty.ML";
     2.7 +use "context.ML";
     2.8 +use "context_position.ML";
     2.9  use "Syntax/lexicon.ML";
    2.10  use "Syntax/simple_syntax.ML";
    2.11 -use "context.ML";
    2.12  use "sorts.ML";
    2.13  use "type.ML";
    2.14  use "config.ML";