isabelle: src/HOL/Reconstruction.thy@cf872f3e16d9 (annotated)

15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	1	(* Title: HOL/Reconstruction.thy
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	2	ID: $Id$
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	3	Author: Lawrence C Paulson
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	4	Copyright 2004 University of Cambridge
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	5	*)
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	6
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	7	header{Attributes for Reconstructing External Resolution Proofs}
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	8
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	9	theory Reconstruction
15872 8336ff711d80 fixed treatment of higher-order simprules paulson parents: 15774 diff changeset	10	imports Hilbert_Choice Map Infinite_Set Extraction
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 16090 diff changeset	11	uses "Tools/res_lib.ML"
15359 8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	12	"Tools/res_clause.ML"
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	13	"Tools/res_skolem_function.ML"
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	14	"Tools/res_axioms.ML"
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	15	"Tools/res_types_sorts.ML"
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	16
16090 fbb5ae140535 goodby to modUnix paulson parents: 16039 diff changeset	17	"Tools/ATP/recon_prelim.ML"
15678 28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	18	"Tools/ATP/recon_order_clauses.ML"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	19	"Tools/ATP/recon_translate_proof.ML"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	20	"Tools/ATP/recon_parse.ML"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	21	"Tools/ATP/recon_transfer_proof.ML"
16479 cf872f3e16d9 use Tools/ATP/VampCommunication.ML; wenzelm parents: 16417 diff changeset	22	"Tools/ATP/VampCommunication.ML"
15678 28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	23	"Tools/ATP/VampireCommunication.ML"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	24	"Tools/ATP/SpassCommunication.ML"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	25	"Tools/ATP/watcher.sig"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	26	"Tools/ATP/watcher.ML"
15700 970e0293dfb3 tweaks mainly to achieve sml/nj compatibility paulson parents: 15684 diff changeset	27	"Tools/ATP/res_clasimpset.ML"
15678 28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	28	"Tools/res_atp.ML"
28cc2314c7ff Reconstruction.thy and IsaMakefile updated quigley parents: 15653 diff changeset	29
16090 fbb5ae140535 goodby to modUnix paulson parents: 16039 diff changeset	30	"Tools/reconstruction.ML"
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	31
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	32	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	33
15382 e56ce5cefe9c all theories must be related to Reconstruction paulson parents: 15359 diff changeset	34	text{Every theory of HOL must be a descendant or ancestor of this one!}
e56ce5cefe9c all theories must be related to Reconstruction paulson parents: 15359 diff changeset	35
16009 a6d480e6c5f0 Skolemization of simprules and classical rules paulson parents: 15872 diff changeset	36	setup ResAxioms.setup
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	37	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	38
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	39	end

author	wenzelm
	Mon, 20 Jun 2005 21:33:27 +0200
changeset 16479	cf872f3e16d9
parent 16417	9bc16273c2d4
child 16563	a92f96951355
permissions	-rw-r--r--