| changeset 5250 | 1bff4b1e5ba9 |
| parent 5199 | be986f7a6def |
| child 5368 | 7c8d1c7c876d |
--- a/src/HOL/ex/ROOT.ML Tue Aug 04 18:24:34 1998 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Aug 04 18:40:18 1998 +0200 @@ -38,5 +38,9 @@ (*Monoids and Groups as predicates over record schemes*) time_use_thy "MonoidGroup"; +(*Groups via locales*) +time_use_thy "PiSets"; +time_use_thy "LocaleGroup"; + writeln "END: Root file for HOL examples";