| author | blanchet |
| Wed, 11 Jul 2012 21:43:19 +0200 | |
| changeset 49265 | 1065c307fafe |
| parent 49249 | 06216c789ac9 |
| child 49299 | a3cb8901d60c |
| permissions | -rw-r--r-- |
1 (* Title: HOL/TPTP/ROOT.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Author: Nik Sultana, University of Cambridge
4 Copyright 2011
6 TPTP-related extensions.
7 *)
9 use_thys [
10 "MaSh_Import",
11 "TPTP_Interpret",
12 "THF_Arith"
13 ];
15 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
16 use_thy "ATP_Problem_Import";