changeset 82360 | 6a09257afd06 |
parent 82343 | 56098b36c49f |
child 82396 | 7230281bde03 |
82359:d2960b321468 | 82360:6a09257afd06 |
---|---|
5 *) |
5 *) |
6 |
6 |
7 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close> |
7 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close> |
8 |
8 |
9 theory Sledgehammer |
9 theory Sledgehammer |
10 imports Presburger SMT Try0 |
10 imports Presburger SMT Try0_HOL |
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 |
15 |