equal
deleted
inserted
replaced
4 Miscellaneous examples for Higher-Order Logic. |
4 Miscellaneous examples for Higher-Order Logic. |
5 *) |
5 *) |
6 |
6 |
7 time_use_thy "Recdefs"; |
7 time_use_thy "Recdefs"; |
8 time_use_thy "Primrec"; |
8 time_use_thy "Primrec"; |
9 (* FIXME time_use_thy "Locales"; *) |
9 time_use_thy "Locales"; |
10 time_use_thy "Records"; |
10 time_use_thy "Records"; |
11 time_use_thy "MonoidGroup"; |
11 time_use_thy "MonoidGroup"; |
12 time_use_thy "StringEx"; |
12 time_use_thy "StringEx"; |
13 time_use_thy "BinEx"; |
13 time_use_thy "BinEx"; |
14 setmp proofs 2 time_use_thy "Hilbert_Classical"; |
14 setmp proofs 2 time_use_thy "Hilbert_Classical"; |