changeset 16417 | 9bc16273c2d4 |
parent 16121 | a80aa66d2271 |
child 16587 | b34c8aa657a5 |
--- a/src/HOL/HOL.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/HOL.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,7 +7,7 @@ theory HOL imports CPure -files ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML") +uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML") ("~~/src/Provers/eqsubst.ML") begin