| changeset 29609 | a010aab5bed0 |
| parent 29580 | 117b88da143c |
| child 29611 | 9891e3646809 |
| 29608:564ea783ace8 | 29609:a010aab5bed0 |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* The Isabelle-ATP Linkup *} |
7 header {* The Isabelle-ATP Linkup *} |
8 |
8 |
9 theory ATP_Linkup |
9 theory ATP_Linkup |
10 imports Record Hilbert_Choice |
10 imports Divides Record Hilbert_Choice |
11 uses |
11 uses |
12 "Tools/polyhash.ML" |
12 "Tools/polyhash.ML" |
13 "Tools/res_clause.ML" |
13 "Tools/res_clause.ML" |
14 ("Tools/res_axioms.ML") |
14 ("Tools/res_axioms.ML") |
15 ("Tools/res_hol_clause.ML") |
15 ("Tools/res_hol_clause.ML") |