isabelle: src/HOL/Reconstruction.thy@0bd9eedaa301 (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
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	11	files "Tools/reconstruction.ML"
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	12
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	13	begin
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	14
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	15	setup Reconstruction.setup
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	16
429666b09783 proof reconstruction for external ATPs paulson parents: diff changeset	17	end

author	nipkow
	Mon, 22 Nov 2004 11:53:56 +0100
changeset 15305	0bd9eedaa301
parent 15151	429666b09783
child 15359	8bad1f42fec0
permissions	-rw-r--r--