| changeset 58481 | 62bc7c79212b |
| parent 58074 | 87a8cc594bf6 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Sledgehammer.thy Mon Sep 29 12:30:12 2014 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Sep 29 14:32:30 2014 +0200 @@ -12,7 +12,7 @@ begin lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y" -by (erule contrapos_nn) (rule arg_cong) + by (erule contrapos_nn) (rule arg_cong) ML_file "Tools/Sledgehammer/async_manager.ML" ML_file "Tools/Sledgehammer/sledgehammer_util.ML"