author | paulson |
Wed, 01 Dec 2004 10:14:10 +0100 | |
changeset 15351 | bdcd0f321df0 |
parent 15350 | 53d2927d9680 |
child 15352 | cba05842bd7a |
src/HOL/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/ROOT.ML Wed Dec 01 06:33:52 2004 +0100 +++ b/src/HOL/ROOT.ML Wed Dec 01 10:14:10 2004 +0100 @@ -39,6 +39,14 @@ with_path "Integ" use_thy "Main"; +(*Linking to external resolution provers*) +use "Tools/res_lib.ML"; +use "Tools/res_clause.ML"; +use "Tools/res_skolem_function.ML"; +use "Tools/res_axioms.ML"; +use "Tools/res_types_sorts.ML"; +use "Tools/res_atp.ML"; + path_add "~~/src/HOL/Library"; print_depth 8;