isabelle: src/HOL/Reconstruction.thy@6e77bd331bf4 (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/res_atp.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	23	"Tools/reconstruction.ML"
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	24
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	25	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	26
16563 a92f96951355 meson method taking an argument list paulson parents: 16479 diff changeset	27	setup ResAxioms.meson_method_setup
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	28	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	29
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	30	end

author	mengj
	Sun, 04 Jun 2006 10:50:41 +0200
changeset 19767	6e77bd331bf4
parent 18794	46d66332bf81
child 20761	7a6f69cf5a86
permissions	-rw-r--r--