isabelle: src/HOL/TPTP/ATP_Problem_Import.thy@d6683fe037b1 (annotated)

46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	1	(* Title: HOL/TPTP/ATP_Problem_Import.thy
e4bccf5ec61e added problem importer blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
e4bccf5ec61e added problem importer blanchet parents: diff changeset	3	*)
e4bccf5ec61e added problem importer blanchet parents: diff changeset	4
e4bccf5ec61e added problem importer blanchet parents: diff changeset	5	header {* ATP Problem Importer *}
e4bccf5ec61e added problem importer blanchet parents: diff changeset	6
e4bccf5ec61e added problem importer blanchet parents: diff changeset	7	theory ATP_Problem_Import
47557 32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools blanchet parents: 46324 diff changeset	8	imports Complex_Main TPTP_Interpret
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	9	uses ("atp_problem_import.ML")
e4bccf5ec61e added problem importer blanchet parents: diff changeset	10	begin
e4bccf5ec61e added problem importer blanchet parents: diff changeset	11
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	12	declare [[show_consts]] (* for Refute *)
24babc4b1925 added timeout argument to TPTP tools blanchet parents: 47557 diff changeset	13
46324 e4bccf5ec61e added problem importer blanchet parents: diff changeset	14	use "atp_problem_import.ML"
e4bccf5ec61e added problem importer blanchet parents: diff changeset	15
e4bccf5ec61e added problem importer blanchet parents: diff changeset	16	end

author	blanchet
	Tue, 24 Apr 2012 09:47:40 +0200
changeset 47714	d6683fe037b1
parent 47670	24babc4b1925
child 47765	18f37b7aa6a6
permissions	-rw-r--r--