equal
deleted
inserted
replaced
73 declare [[ |
73 declare [[ |
74 tptp_unexceptional_reconstruction = false, (*NOTE should be "false" while testing*) |
74 tptp_unexceptional_reconstruction = false, (*NOTE should be "false" while testing*) |
75 tptp_informative_failure = true |
75 tptp_informative_failure = true |
76 ]] |
76 ]] |
77 |
77 |
78 ML_file "TPTP_Parser/tptp_reconstruct_library.ML" |
78 ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close> |
79 ML "open TPTP_Reconstruct_Library" |
79 ML "open TPTP_Reconstruct_Library" |
80 ML_file "TPTP_Parser/tptp_reconstruct.ML" |
80 ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close> |
81 |
81 |
82 (*FIXME fudge*) |
82 (*FIXME fudge*) |
83 declare [[ |
83 declare [[ |
84 blast_depth_limit = 10, |
84 blast_depth_limit = 10, |
85 unify_search_bound = 5 |
85 unify_search_bound = 5 |