isabelle: src/HOL/Reconstruction.thy@61a430a67d7c (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
17819 1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	11	uses "Tools/res_clause.ML"
18004 1883971957de Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses. mengj parents: 17846 diff changeset	12	"Tools/res_hol_clause.ML"
17819 1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	13	"Tools/res_axioms.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	14	"Tools/ATP/recon_order_clauses.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	15	"Tools/ATP/recon_translate_proof.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	16	"Tools/ATP/recon_parse.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	17	"Tools/ATP/recon_transfer_proof.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	18	"Tools/ATP/AtpCommunication.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	19	"Tools/ATP/watcher.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	20	"Tools/ATP/res_clasimpset.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	21	"Tools/res_atp.ML"
1241e5d31d5b small tidy-up of utility functions paulson parents: 17603 diff changeset	22	"Tools/reconstruction.ML"
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	23
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	24	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	25
16563 a92f96951355 meson method taking an argument list paulson parents: 16479 diff changeset	26	setup ResAxioms.meson_method_setup
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	27	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	28
15653 3549ff7158f3 Updated to add watcher code. quigley parents: 15645 diff changeset	29	end

author	wenzelm
	Tue, 08 Nov 2005 10:43:08 +0100
changeset 18117	61a430a67d7c
parent 18004	1883971957de
child 18449	e314fb38307d
permissions	-rw-r--r--