| author | huffman |
| Fri, 08 Oct 2010 07:39:50 -0700 | |
| changeset 39986 | 38677db30cad |
| parent 39958 | 88c9aa5666de |
| child 40121 | e7a80c6752c9 |
| 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 |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
9 |
imports Plain |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
10 |
uses "Tools/ATP/atp_problem.ML" |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
11 |
"Tools/ATP/atp_proof.ML" |
|
ff60a6e4edfe
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
blanchet
parents:
diff
changeset
|
12 |
"Tools/ATP/atp_systems.ML" |
|
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 |