changeset 20809 | 6c4fd0b4b63a |
parent 20788 | d51711512d07 |
child 20862 | 1059f2316f88 |
--- a/src/HOL/Reconstruction.thy Sun Oct 01 18:29:25 2006 +0200 +++ b/src/HOL/Reconstruction.thy Sun Oct 01 18:29:26 2006 +0200 @@ -7,7 +7,7 @@ header{* Reconstructing external resolution proofs *} theory Reconstruction -imports Hilbert_Choice Map Infinite_Set Extraction +imports Hilbert_Choice Map Extraction uses "Tools/polyhash.ML" "Tools/ATP/AtpCommunication.ML" "Tools/ATP/watcher.ML"