src/HOL/TPTP/ATP_Problem_Import.thy
author blanchet
Mon Jan 23 17:40:32 2012 +0100 (2012-01-23)
changeset 46324 e4bccf5ec61e
child 47557 32f35b3d9e42
permissions -rw-r--r--
added problem importer
blanchet@46324
     1
(*  Title:      HOL/TPTP/ATP_Problem_Import.thy
blanchet@46324
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@46324
     3
*)
blanchet@46324
     4
blanchet@46324
     5
header {* ATP Problem Importer *}
blanchet@46324
     6
blanchet@46324
     7
theory ATP_Problem_Import
blanchet@46324
     8
imports Complex_Main
blanchet@46324
     9
uses ("atp_problem_import.ML")
blanchet@46324
    10
begin
blanchet@46324
    11
blanchet@46324
    12
typedecl iota (* for TPTP *)
blanchet@46324
    13
blanchet@46324
    14
use "atp_problem_import.ML"
blanchet@46324
    15
blanchet@46324
    16
end