resolution package tools by Jia Meng
authorpaulson
Wed Dec 01 10:14:10 2004 +0100 (2004-12-01)
changeset 15351bdcd0f321df0
parent 15350 53d2927d9680
child 15352 cba05842bd7a
resolution package tools by Jia Meng
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Wed Dec 01 06:33:52 2004 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Dec 01 10:14:10 2004 +0100
     1.3 @@ -39,6 +39,14 @@
     1.4  
     1.5  with_path "Integ" use_thy "Main";
     1.6  
     1.7 +(*Linking to external resolution provers*)
     1.8 +use "Tools/res_lib.ML";
     1.9 +use "Tools/res_clause.ML";
    1.10 +use "Tools/res_skolem_function.ML";
    1.11 +use "Tools/res_axioms.ML";
    1.12 +use "Tools/res_types_sorts.ML";
    1.13 +use "Tools/res_atp.ML";
    1.14 +
    1.15  path_add "~~/src/HOL/Library";
    1.16  
    1.17  print_depth 8;