| changeset 17421 | 0382f6877b98 |
| parent 17315 | 5bf0e0aacc24 |
| child 17462 | 47f7bddc3239 |
--- a/src/HOL/Reconstruction.thy Thu Sep 15 17:44:53 2005 +0200 +++ b/src/HOL/Reconstruction.thy Thu Sep 15 17:45:17 2005 +0200 @@ -7,7 +7,7 @@ header{*Attributes for Reconstructing External Resolution Proofs*} theory Reconstruction - imports Hilbert_Choice Map Infinite_Set Extraction + imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction uses "Tools/res_lib.ML" "Tools/res_clause.ML"