| changeset 17508 | c84af7f39a6b |
| parent 17488 | 67376a311a2b |
| child 17603 | f601609d3300 |
--- a/src/HOL/Reconstruction.thy Tue Sep 20 13:58:58 2005 +0200 +++ b/src/HOL/Reconstruction.thy Tue Sep 20 14:03:37 2005 +0200 @@ -7,7 +7,7 @@ header{* Reconstructing external resolution proofs *} theory Reconstruction -imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction +imports Hilbert_Choice Map Infinite_Set Extraction uses "Tools/res_lib.ML" "Tools/res_clause.ML"