removed obsolete install_pp.ML (cf. pure_setup.ML);
authorwenzelm
Sun Jul 29 16:00:00 2007 +0200 (2007-07-29)
changeset 2405290dd4df2c7c3
parent 24051 896fb015079c
child 24053 af1dd276fae0
removed obsolete install_pp.ML (cf. pure_setup.ML);
src/Pure/IsaMakefile
src/Pure/install_pp.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun Jul 29 14:30:07 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sun Jul 29 16:00:00 2007 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4    Tools/nbe_eval.ML Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML 	\
     1.5    codegen.ML compress.ML config_option.ML conjunction.ML consts.ML context.ML	\
     1.6    context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
     1.7 -  fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML	\
     1.8 +  fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML	\
     1.9    more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML	\
    1.10    pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
    1.11    tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML		\
     2.1 --- a/src/Pure/install_pp.ML	Sun Jul 29 14:30:07 2007 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,15 +0,0 @@
     2.4 -(*  Title:      Pure/install_pp.ML
     2.5 -    ID:         $Id$
     2.6 -
     2.7 -ML toplevel pretty printing.
     2.8 -*)
     2.9 -
    2.10 -install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
    2.11 -install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
    2.12 -install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
    2.13 -install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
    2.14 -install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
    2.15 -install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    2.16 -install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
    2.17 -install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
    2.18 -install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));