removed obsolete proof_general.ML;
authorwenzelm
Fri Dec 29 18:46:01 2006 +0100 (2006-12-29)
changeset 2194162dd79056d70
parent 21940 fbd068dd4d29
child 21942 d6218d0f9ec3
removed obsolete proof_general.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Dec 29 18:25:46 2006 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Fri Dec 29 18:46:01 2006 +0100
     1.3 @@ -67,9 +67,9 @@
     1.4    conjunction.ML consts.ML context.ML defs.ML display.ML drule.ML		\
     1.5    envir.ML fact_index.ML goal.ML install_pp.ML library.ML logic.ML		\
     1.6    meta_simplifier.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML		\
     1.7 -  proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML			\
     1.8 -  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML		\
     1.9 -  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
    1.10 +  proofterm.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		\
    1.12 +  type_infer.ML unify.ML variable.ML
    1.13  	@./mk
    1.14  
    1.15  
     2.1 --- a/src/Pure/ROOT.ML	Fri Dec 29 18:25:46 2006 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Fri Dec 29 18:46:01 2006 +0100
     2.3 @@ -83,12 +83,7 @@
     2.4  cd "Tools"; use "ROOT.ML"; cd "..";
     2.5  
     2.6  (*configuration for Proof General*)
     2.7 -(* Next line is OLD CODE: in case you have problems, uncomment next line and 
     2.8 -   comment out line after. Please report any problems to da@inf.ed.ac.uk.
     2.9 -   Plan is to remove old code very soon. *)
    2.10 -(*(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; *)
    2.11 -(* Next line is NEW CODE.  Hopefully now working on SMLNJ and Poly/ML. *)
    2.12 -cd "ProofGeneral"; use "ROOT.ML"; cd ".."; 
    2.13 +cd "ProofGeneral"; use "ROOT.ML"; cd "..";
    2.14  
    2.15  use_thy "Pure";
    2.16  structure Pure = struct val thy = theory "Pure" end;