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

15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	1	(* Title: HOL/Reconstruction.thy
17603 f601609d3300 spaces inserted in header webertj parents: 17508 diff changeset	2	ID: $Id$
15151 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
17462 47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	7	header{* Reconstructing external resolution proofs *}
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	8
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	9	theory Reconstruction
17508 c84af7f39a6b tuned theory dependencies; wenzelm parents: 17488 diff changeset	10	imports Hilbert_Choice Map Infinite_Set Extraction
18449 e314fb38307d new hash table module in HOL/Too/s paulson parents: 18004 diff changeset	11	uses "Tools/polyhash.ML"
e314fb38307d new hash table module in HOL/Too/s paulson parents: 18004 diff changeset	12	"Tools/res_clause.ML"
e314fb38307d new hash table module in HOL/Too/s paulson parents: 18004 diff changeset	13	"Tools/res_hol_clause.ML"
17819 1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	14	"Tools/res_axioms.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	15	"Tools/ATP/recon_order_clauses.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	16	"Tools/ATP/recon_translate_proof.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	17	"Tools/ATP/recon_parse.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	18	"Tools/ATP/recon_transfer_proof.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	19	"Tools/ATP/AtpCommunication.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	20	"Tools/ATP/watcher.ML"
18794 46d66332bf81 Added new file Tools/ATP/reduce_axiomsN.ML mengj parents: 18449 diff changeset	21	"Tools/ATP/reduce_axiomsN.ML"
17819 1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	22	"Tools/ATP/res_clasimpset.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	23	"Tools/res_atp.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	24	"Tools/reconstruction.ML"
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	25
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	26	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	27
16563 a92f96951355 meson method taking an argument list paulson parents: 16479 diff changeset	28	setup ResAxioms.meson_method_setup
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	29	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	30
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	31	end

author	paulson
	Wed, 19 Apr 2006 10:42:13 +0200
changeset 19446	30e1178d7a3b
parent 18794	46d66332bf81
child 19767	6e77bd331bf4
permissions	-rw-r--r--