isabelle: src/HOL/Reconstruction.thy@fc385ce6187d (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
17462 47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	11	uses "Tools/res_lib.ML"
17236 6edb84c661dd Added ECommunication.ML quigley parents: 17229 diff changeset	12
17462 47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	13	"Tools/res_clause.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	14	"Tools/res_skolem_function.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	15	"Tools/res_axioms.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	16	"Tools/res_types_sorts.ML"
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	17
17462 47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	18	"Tools/ATP/recon_order_clauses.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	19	"Tools/ATP/recon_translate_proof.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	20	"Tools/ATP/recon_parse.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	21	"Tools/ATP/recon_transfer_proof.ML"
17484 f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems paulson parents: 17462 diff changeset	22	"Tools/ATP/AtpCommunication.ML"
17462 47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	23	"Tools/ATP/watcher.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	24	"Tools/ATP/res_clasimpset.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	25	"Tools/res_atp.ML"
47f7bddc3239 moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories); wenzelm parents: 17421 diff changeset	26	"Tools/reconstruction.ML"
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	27
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	28	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	29
16563 a92f96951355 meson method taking an argument list paulson parents: 16479 diff changeset	30	setup ResAxioms.meson_method_setup
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	31	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	32
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	33	end

author	aspinall
	Fri, 30 Sep 2005 18:18:34 +0200
changeset 17740	fc385ce6187d
parent 17603	f601609d3300
child 17819	1241e5d31d5b
permissions	-rw-r--r--