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 ATP |
10 imports ATP Metis |
11 uses "Tools/Sledgehammer/sledgehammer_util.ML" |
11 uses "Tools/Sledgehammer/sledgehammer_util.ML" |
12 "Tools/Sledgehammer/sledgehammer_filter.ML" |
12 "Tools/Sledgehammer/sledgehammer_filter.ML" |
13 "Tools/Sledgehammer/sledgehammer_atp_translate.ML" |
13 "Tools/Sledgehammer/sledgehammer_atp_translate.ML" |
14 "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" |
14 "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML" |
15 "Tools/Sledgehammer/sledgehammer.ML" |
15 "Tools/Sledgehammer/sledgehammer.ML" |