--- a/src/HOL/Reconstruction.thy Tue Dec 07 16:15:44 2004 +0100
+++ b/src/HOL/Reconstruction.thy Tue Dec 07 16:16:10 2004 +0100
@@ -7,7 +7,7 @@
header{*Attributes for Reconstructing External Resolution Proofs*}
theory Reconstruction
- imports Hilbert_Choice
+ imports Hilbert_Choice Map Infinite_Set
files "Tools/res_lib.ML"
"Tools/res_clause.ML"
"Tools/res_skolem_function.ML"
@@ -18,6 +18,8 @@
begin
+text{*Every theory of HOL must be a descendant or ancestor of this one!*}
+
setup Reconstruction.setup
end
\ No newline at end of file