src/HOL/Reconstruction.thy
changeset 15151 429666b09783
child 15359 8bad1f42fec0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Reconstruction.thy	Fri Aug 20 12:21:03 2004 +0200
@@ -0,0 +1,17 @@
+(*  Title:      HOL/Reconstruction.thy
+    ID: $Id$
+    Author:     Lawrence C Paulson
+    Copyright   2004  University of Cambridge
+*)
+
+header{*Attributes for Reconstructing External Resolution Proofs*}
+
+theory Reconstruction
+    imports Hilbert_Choice
+    files   "Tools/reconstruction.ML"
+
+begin
+
+setup Reconstruction.setup
+
+end
\ No newline at end of file