added context_position.ML;
authorwenzelm
Wed Jun 13 00:01:56 2007 +0200 (2007-06-13)
changeset 233533069dade3eb4
parent 23352 356edb5eb1c4
child 23354 a189707c1d76
added context_position.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Jun 13 00:01:54 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Wed Jun 13 00:01:56 2007 +0200
     1.3 @@ -64,11 +64,12 @@
     1.4    Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML		\
     1.5    Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml_syntax.ML 	\
     1.6    assumption.ML axclass.ML codegen.ML compress.ML conjunction.ML consts.ML 	\
     1.7 -  context.ML conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML	\
     1.8 -  install_pp.ML library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML 	\
     1.9 -  name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_thy.ML search.ML 	\
    1.10 -  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML 	\
    1.11 -  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
    1.12 +  context.ML context_position.ML conv.ML defs.ML display.ML drule.ML		\
    1.13 +  envir.ML fact_index.ML goal.ML install_pp.ML library.ML logic.ML		\
    1.14 +  meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML old_goals.ML	\
    1.15 +  pattern.ML proofterm.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML	\
    1.16 +  subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML	\
    1.17 +  type.ML type_infer.ML unify.ML variable.ML
    1.18  	@./mk
    1.19  
    1.20  
     2.1 --- a/src/Pure/ROOT.ML	Wed Jun 13 00:01:54 2007 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Wed Jun 13 00:01:56 2007 +0200
     2.3 @@ -28,6 +28,7 @@
     2.4  use "sorts.ML";
     2.5  use "type.ML";
     2.6  use "context.ML";
     2.7 +use "context_position.ML";
     2.8  use "compress.ML";
     2.9  use "type_infer.ML";
    2.10