| changeset 72399 | f8900a5ad4a7 | 
| parent 71793 | e771b8157fc7 | 
| child 72588 | c7e2a9bdc585 | 
--- a/src/HOL/ATP.thy Thu Oct 08 16:07:10 2020 +0200 +++ b/src/HOL/ATP.thy Thu Oct 08 16:36:00 2020 +0200 @@ -15,7 +15,6 @@ ML_file \<open>Tools/ATP/atp_problem.ML\<close> ML_file \<open>Tools/ATP/atp_proof.ML\<close> ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close> -ML_file \<open>Tools/ATP/atp_satallax.ML\<close> subsection \<open>Higher-order reasoning helpers\<close>