equal
deleted
inserted
replaced
10 imports Presburger SMT |
10 imports Presburger SMT |
11 keywords |
11 keywords |
12 "sledgehammer" :: diag and |
12 "sledgehammer" :: diag and |
13 "sledgehammer_params" :: thy_decl |
13 "sledgehammer_params" :: thy_decl |
14 begin |
14 begin |
15 |
|
16 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y" |
|
17 by (erule contrapos_nn) (rule arg_cong) |
|
18 |
15 |
19 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close> |
16 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close> |
20 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close> |
17 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close> |
21 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close> |
18 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close> |
22 ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close> |
19 ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close> |