proper loading of ML files (in HOL.thy);
authorwenzelm
Thu May 31 18:16:57 2007 +0200 (2007-05-31)
changeset 2316645f3c90b2d27
parent 23165 5d319b0f8bf9
child 23167 b9bbdf7eab3b
proper loading of ML files (in HOL.thy);
moved Integ files to canonical place;
misc cleanup;
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Thu May 31 18:16:54 2007 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Thu May 31 18:16:57 2007 +0200
     1.3 @@ -1,44 +1,11 @@
     1.4  (*  Title:      HOL/ROOT.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1993  University of Cambridge
     1.8 -
     1.9 + 
    1.10  Classical Higher-order Logic.
    1.11  *)
    1.12  
    1.13 -val banner = "Higher-Order Logic";
    1.14 -writeln banner;
    1.15 -
    1.16 -use "hologic.ML";
    1.17 -
    1.18 -use "~~/src/Provers/splitter.ML";
    1.19 -use "~~/src/Provers/hypsubst.ML";
    1.20 -use "~~/src/Provers/IsaPlanner/zipper.ML";
    1.21 -use "~~/src/Provers/IsaPlanner/isand.ML";
    1.22 -use "~~/src/Provers/IsaPlanner/rw_tools.ML";
    1.23 -use "~~/src/Provers/IsaPlanner/rw_inst.ML";
    1.24 -use "~~/src/Provers/eqsubst.ML";
    1.25 -use "~~/src/Provers/induct_method.ML";
    1.26 -use "~~/src/Provers/classical.ML";
    1.27 -use "~~/src/Provers/blast.ML";
    1.28 -use "~~/src/Provers/clasimp.ML";
    1.29 -use "~~/src/Pure/General/int.ML";
    1.30 -use "~~/src/Pure/General/rat.ML";
    1.31 -use "~~/src/Provers/Arith/fast_lin_arith.ML";
    1.32 -use "~~/src/Provers/Arith/cancel_sums.ML";
    1.33 -use "~~/src/Provers/quantifier1.ML";
    1.34 -use "~~/src/Provers/project_rule.ML";
    1.35 -use "~~/src/Provers/Arith/cancel_numerals.ML";
    1.36 -use "~~/src/Provers/Arith/combine_numerals.ML";
    1.37 -use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
    1.38 -use "~~/src/Provers/Arith/extract_common_term.ML";
    1.39 -use "~~/src/Provers/quasi.ML";
    1.40 -use "~~/src/Provers/order.ML";
    1.41 -
    1.42 -with_path "Integ" use_thy "Main";
    1.43 +use_thy "Main";
    1.44  
    1.45  path_add "~~/src/HOL/Library";
    1.46  
    1.47  Goal "True";  (*leave subgoal package empty*)
    1.48 -
    1.49 -val HOL_proofs = !proofs;