added conv.ML;
authorwenzelm
Thu May 10 00:39:50 2007 +0200 (2007-05-10)
changeset 22904de2d630e1548
parent 22903 95ad1a91ecef
child 22905 dab6a898b47c
added conv.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Thu May 10 00:39:49 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu May 10 00:39:50 2007 +0200
     1.3 @@ -63,9 +63,9 @@
     1.4    Tools/codegen_names.ML Tools/codegen_package.ML Tools/codegen_serializer.ML	\
     1.5    Tools/codegen_thingol.ML Tools/compute.ML Tools/invoke.ML Tools/nbe.ML 	\
     1.6    Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml_syntax.ML assumption.ML	\
     1.7 -  axclass.ML codegen.ML compress.ML conjunction.ML consts.ML context.ML defs.ML	\
     1.8 -  display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML 	\
     1.9 -  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML		\
    1.10 +  axclass.ML codegen.ML compress.ML conjunction.ML consts.ML context.ML conv.ML \
    1.11 +  defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML 	\
    1.12 +  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
    1.13    old_goals.ML pattern.ML proofterm.ML pure_thy.ML search.ML sign.ML		\
    1.14    simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML	\
    1.15    theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
     2.1 --- a/src/Pure/ROOT.ML	Thu May 10 00:39:49 2007 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Thu May 10 00:39:50 2007 +0200
     2.3 @@ -70,6 +70,7 @@
     2.4  use "pure_thy.ML";
     2.5  use "display.ML";
     2.6  use "drule.ML";
     2.7 +use "conv.ML";
     2.8  use "morphism.ML";
     2.9  use "variable.ML";
    2.10  use "tctical.ML";