equal
deleted
inserted
replaced
1 (* Title: HOL/ATP.thy |
1 (* Title: HOL/ATP.thy |
2 Author: Fabian Immler, TU Muenchen |
2 Author: Fabian Immler, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Sledgehammer: Isabelle--ATP Linkup *} |
6 header {* Automatic Theorem Provers (ATPs) *} |
7 |
7 |
8 theory ATP |
8 theory ATP |
9 imports Plain |
9 imports Plain |
10 uses "Tools/ATP/atp_problem.ML" |
10 uses "Tools/ATP/atp_problem.ML" |
11 "Tools/ATP/atp_proof.ML" |
11 "Tools/ATP/atp_proof.ML" |