--- a/src/HOL/Sledgehammer.thy Fri Oct 25 14:51:16 2019 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Oct 25 14:55:14 2019 +0200
@@ -16,6 +16,8 @@
lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
by (erule contrapos_nn) (rule arg_cong)
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
+
ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
@@ -35,4 +37,7 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
+lemma "1 + 1 = 2"
+ sledgehammer [iprover, overlord, dont_minimize, dont_preplay]
+
end