# HG changeset patch
# User paulson
# Date 1101892450 -3600
# Node ID bdcd0f321df0a30f69a69d8fae3bffa54f88cb31
# Parent  53d2927d9680f80b19e662884e0f31b45a7e153e
resolution package tools by Jia Meng

diff -r 53d2927d9680 -r bdcd0f321df0 src/HOL/ROOT.ML
--- 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;