removed obsolete compress.ML
authorwenzelm
Sat Apr 12 17:00:42 2008 +0200 (2008-04-12)
changeset 266296e93fbd4c96a
parent 26628 63306cb94313
child 26630 3074b3de4f4f
removed obsolete compress.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Sat Apr 12 17:00:40 2008 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sat Apr 12 17:00:42 2008 +0200
     1.3 @@ -71,10 +71,10 @@
     1.4    Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
     1.5    Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML			\
     1.6    Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
     1.7 -  assumption.ML axclass.ML codegen.ML compress.ML config.ML		\
     1.8 -  conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML	\
     1.9 -  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
    1.10 -  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    1.11 +  assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
    1.12 +  consts.ML context.ML conv.ML defs.ML display.ML drule.ML envir.ML	\
    1.13 +  facts.ML goal.ML interpretation.ML library.ML logic.ML		\
    1.14 +  meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML		\
    1.15    old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML	\
    1.16    pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
    1.17    tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML	\
     2.1 --- a/src/Pure/ROOT.ML	Sat Apr 12 17:00:40 2008 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sat Apr 12 17:00:42 2008 +0200
     2.3 @@ -34,7 +34,6 @@
     2.4  use "type.ML";
     2.5  use "type_infer.ML";
     2.6  use "config.ML";
     2.7 -use "compress.ML";
     2.8  
     2.9  (*inner syntax module*)
    2.10  use "Syntax/ast.ML";