isabelle: src/HOL/Reconstruction.thy@8bad1f42fec0 (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
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	10	imports Hilbert_Choice
15359 8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	11	files "Tools/res_lib.ML"
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"
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	16	"Tools/res_atp.ML"
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas paulson parents: 15151 diff changeset	17	"Tools/reconstruction.ML"
15151 429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	18
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	19	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	20
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	21	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	22
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	23	end

author	paulson
	Thu, 02 Dec 2004 11:09:19 +0100
changeset 15359	8bad1f42fec0
parent 15151	429666b09783
child 15382	e56ce5cefe9c
permissions	-rw-r--r--