equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Sledgehammer: Isabelle--ATP Linkup *} |
7 header {* Sledgehammer: Isabelle--ATP Linkup *} |
8 |
8 |
9 theory Sledgehammer |
9 theory Sledgehammer |
10 imports Presburger ATP SMT2 |
10 imports Presburger SMT2 |
11 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
11 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
12 begin |
12 begin |
13 |
13 |
14 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y" |
14 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y" |
15 by (erule contrapos_nn) (rule arg_cong) |
15 by (erule contrapos_nn) (rule arg_cong) |