| author | blanchet |
| Sun, 22 Apr 2012 14:16:46 +0200 | |
| changeset 47670 | 24babc4b1925 |
| parent 47557 | 32f35b3d9e42 |
| child 47714 | d6683fe037b1 |
| permissions | -rw-r--r-- |
(* Title: HOL/TPTP/ATP_Problem_Import.thy Author: Jasmin Blanchette, TU Muenchen *) header {* ATP Problem Importer *} theory ATP_Problem_Import imports Complex_Main TPTP_Interpret uses ("atp_problem_import.ML") begin declare [[show_consts]] (* for Refute *) typedecl iota (* for TPTP *) use "atp_problem_import.ML" end