author | wenzelm |
Sun, 01 Oct 2006 18:29:31 +0200 | |
changeset 20812 | cc6b31c2b9a2 |
parent 20811 | eccbfaf2bc0e |
child 20813 | 379ce56e5dc2 |
--- a/src/HOL/ex/ROOT.ML Sun Oct 01 18:29:30 2006 +0200 +++ b/src/HOL/ex/ROOT.ML Sun Oct 01 18:29:31 2006 +0200 @@ -20,12 +20,12 @@ time_use_thy "Locales"; time_use_thy "Records"; time_use_thy "MonoidGroup"; -time_use_thy "StringEx"; time_use_thy "BinEx"; setmp proofs 2 time_use_thy "Hilbert_Classical"; time_use_thy "Antiquote"; time_use_thy "Multiquote"; +time_use_thy "PER"; time_use_thy "NatSum"; time_use_thy "ThreeDivides"; time_use_thy "Intuitionistic";