src/HOL/ATP.thy
changeset 57707 0242e9578828
parent 57263 2b6a96cc64c9
child 57709 9cda0c64c37a
--- a/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
@@ -15,6 +15,8 @@
 ML_file "Tools/ATP/atp_problem.ML"
 ML_file "Tools/ATP/atp_proof.ML"
 ML_file "Tools/ATP/atp_proof_redirect.ML"
+ML_file "Tools/ATP/atp_satallax.ML"
+
 
 subsection {* Higher-order reasoning helpers *}