author | bulwahn |
Mon, 12 Dec 2011 13:45:54 +0100 | |
changeset 45818 | 53a697f5454a |
parent 43804 | eb9be23db2b7 |
child 46321 | 484dc68c8c89 |
permissions | -rw-r--r-- |
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/TPTP/ROOT.ML |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
3 |
Author: Nik Sultana, University of Cambridge |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
4 |
Copyright 2011 |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
5 |
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
6 |
TPTP-related extensions. |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
7 |
*) |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
8 |
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
9 |
use_thys [ |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
10 |
"ATP_Export" |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
11 |
]; |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
12 |
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
13 |
Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs) |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
14 |
use_thy "CASC_Setup"; |