author | wenzelm |
Sun, 20 May 2012 11:34:33 +0200 | |
changeset 47884 | 21c42b095c84 |
parent 47792 | 804fdf0f6006 |
child 48234 | 06216c789ac9 |
permissions | -rw-r--r-- |
(* Title: HOL/TPTP/ROOT.ML Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions. *) use_thys [ "ATP_Theory_Export", "TPTP_Interpret", "THF_Arith" ]; Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs) use_thy "ATP_Problem_Import";