equal
deleted
inserted
replaced
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 PreList Hilbert_Choice |
10 imports Record Presburger SAT Recdef Extraction Relation_Power Hilbert_Choice |
11 (*FIXME It must be a parent or a child of every other theory, to prevent theory-merge errors. FIXME*) |
11 (*FIXME It must be a parent or a child of every other theory, to prevent theory-merge errors. FIXME*) |
12 uses |
12 uses |
13 "Tools/polyhash.ML" |
13 "Tools/polyhash.ML" |
14 "Tools/res_clause.ML" |
14 "Tools/res_clause.ML" |
15 ("Tools/res_hol_clause.ML") |
15 ("Tools/res_hol_clause.ML") |