| author | blanchet |
| Fri, 27 May 2011 10:30:08 +0200 | |
| changeset 43016 | 42330f25142c |
| parent 40178 | 00152d17855b |
| child 43085 | 0a2f5b86bdd7 |
| permissions | -rw-r--r-- |
|
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/ATP.thy |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
2 |
Author: Fabian Immler, TU Muenchen |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
4 |
*) |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
5 |
|
| 39958 | 6 |
header {* Automatic Theorem Provers (ATPs) *}
|
|
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
7 |
|
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
8 |
theory ATP |
|
40178
00152d17855b
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset
|
9 |
imports Plain |
|
00152d17855b
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset
|
10 |
uses "Tools/ATP/atp_problem.ML" |
|
00152d17855b
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset
|
11 |
"Tools/ATP/atp_proof.ML" |
|
00152d17855b
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset
|
12 |
"Tools/ATP/atp_systems.ML" |
|
39951
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
13 |
begin |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
14 |
|
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
15 |
setup ATP_Systems.setup |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
16 |
|
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
17 |
end |