--- a/src/HOL/Sledgehammer.thy Thu Oct 08 17:47:35 2020 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Oct 08 17:55:17 2020 +0200
@@ -13,9 +13,6 @@
"sledgehammer_params" :: thy_decl
begin
-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/Sledgehammer/async_manager_legacy.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>