changeset 8917 | 2ff6f8693c4f |
parent 7019 | 71f2155cdd85 |
child 9000 | c20d58286a51 |
--- a/src/HOL/Induct/ROOT.ML Mon May 22 12:35:02 2000 +0200 +++ b/src/HOL/Induct/ROOT.ML Mon May 22 12:35:34 2000 +0200 @@ -13,7 +13,7 @@ time_use_thy "Comb"; time_use_thy "Mutil"; time_use_thy "Acc"; -time_use_thy "Multiset"; +time_use_thy "MultisetOrder"; time_use_thy "PropLog"; time_use_thy "SList"; time_use_thy "LFilter";