| changeset 18004 | 1883971957de |
| parent 17846 | 6fd3261a1be0 |
| child 18449 | e314fb38307d |
--- a/src/HOL/Reconstruction.thy Fri Oct 28 02:29:01 2005 +0200 +++ b/src/HOL/Reconstruction.thy Fri Oct 28 02:30:12 2005 +0200 @@ -9,6 +9,7 @@ theory Reconstruction imports Hilbert_Choice Map Infinite_Set Extraction uses "Tools/res_clause.ML" + "Tools/res_hol_clause.ML" "Tools/res_axioms.ML" "Tools/ATP/recon_order_clauses.ML" "Tools/ATP/recon_translate_proof.ML"