equal
deleted
inserted
replaced
6 |
6 |
7 header {* Sledgehammer: Isabelle--ATP Linkup *} |
7 header {* Sledgehammer: Isabelle--ATP Linkup *} |
8 |
8 |
9 theory Sledgehammer |
9 theory Sledgehammer |
10 imports ATP SMT |
10 imports ATP SMT |
|
11 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl |
11 uses "Tools/Sledgehammer/async_manager.ML" |
12 uses "Tools/Sledgehammer/async_manager.ML" |
12 "Tools/Sledgehammer/sledgehammer_util.ML" |
13 "Tools/Sledgehammer/sledgehammer_util.ML" |
13 "Tools/Sledgehammer/sledgehammer_filter.ML" |
14 "Tools/Sledgehammer/sledgehammer_filter.ML" |
14 "Tools/Sledgehammer/sledgehammer_provers.ML" |
15 "Tools/Sledgehammer/sledgehammer_provers.ML" |
15 "Tools/Sledgehammer/sledgehammer_minimize.ML" |
16 "Tools/Sledgehammer/sledgehammer_minimize.ML" |