# HG changeset patch # User wenzelm # Date 1180628217 -7200 # Node ID 45f3c90b2d27e0eecc38a0ce8045af92092504e3 # Parent 5d319b0f8bf9809b5bb7bdb89a6a633adf7ac258 proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup; diff -r 5d319b0f8bf9 -r 45f3c90b2d27 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Thu May 31 18:16:54 2007 +0200 +++ b/src/HOL/ROOT.ML Thu May 31 18:16:57 2007 +0200 @@ -1,44 +1,11 @@ (* Title: HOL/ROOT.ML ID: $Id$ - Author: Tobias Nipkow - Copyright 1993 University of Cambridge - + Classical Higher-order Logic. *) -val banner = "Higher-Order Logic"; -writeln banner; - -use "hologic.ML"; - -use "~~/src/Provers/splitter.ML"; -use "~~/src/Provers/hypsubst.ML"; -use "~~/src/Provers/IsaPlanner/zipper.ML"; -use "~~/src/Provers/IsaPlanner/isand.ML"; -use "~~/src/Provers/IsaPlanner/rw_tools.ML"; -use "~~/src/Provers/IsaPlanner/rw_inst.ML"; -use "~~/src/Provers/eqsubst.ML"; -use "~~/src/Provers/induct_method.ML"; -use "~~/src/Provers/classical.ML"; -use "~~/src/Provers/blast.ML"; -use "~~/src/Provers/clasimp.ML"; -use "~~/src/Pure/General/int.ML"; -use "~~/src/Pure/General/rat.ML"; -use "~~/src/Provers/Arith/fast_lin_arith.ML"; -use "~~/src/Provers/Arith/cancel_sums.ML"; -use "~~/src/Provers/quantifier1.ML"; -use "~~/src/Provers/project_rule.ML"; -use "~~/src/Provers/Arith/cancel_numerals.ML"; -use "~~/src/Provers/Arith/combine_numerals.ML"; -use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; -use "~~/src/Provers/Arith/extract_common_term.ML"; -use "~~/src/Provers/quasi.ML"; -use "~~/src/Provers/order.ML"; - -with_path "Integ" use_thy "Main"; +use_thy "Main"; path_add "~~/src/HOL/Library"; Goal "True"; (*leave subgoal package empty*) - -val HOL_proofs = !proofs;