author | blanchet |
Wed, 18 Jul 2012 08:44:03 +0200 | |
changeset 48297 | dcf3160376ae |
parent 48284 | a3cb8901d60c |
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 [ |
48284 | 10 |
"ATP_Theory_Export", |
48297 | 11 |
"MaSh_Eval", |
48284 | 12 |
"MaSh_Export", |
47792
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47526
diff
changeset
|
13 |
"TPTP_Interpret", |
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47526
diff
changeset
|
14 |
"THF_Arith" |
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
15 |
]; |
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
16 |
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
diff
changeset
|
17 |
Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs) |
47792
804fdf0f6006
get rid of old CASC setup and move the arithmetic part to a new theory
blanchet
parents:
47526
diff
changeset
|
18 |
use_thy "ATP_Problem_Import"; |