| changeset 5250 | 1bff4b1e5ba9 |
| parent 5199 | be986f7a6def |
| child 5368 | 7c8d1c7c876d |
| 5249:9d7e6f7110ef | 5250:1bff4b1e5ba9 |
|---|---|
36 time_use_thy "BinEx"; |
36 time_use_thy "BinEx"; |
37 |
37 |
38 (*Monoids and Groups as predicates over record schemes*) |
38 (*Monoids and Groups as predicates over record schemes*) |
39 time_use_thy "MonoidGroup"; |
39 time_use_thy "MonoidGroup"; |
40 |
40 |
41 (*Groups via locales*) |
|
42 time_use_thy "PiSets"; |
|
43 time_use_thy "LocaleGroup"; |
|
44 |
|
41 |
45 |
42 writeln "END: Root file for HOL examples"; |
46 writeln "END: Root file for HOL examples"; |