| author | berghofe |
| Mon, 10 Dec 2001 15:36:05 +0100 | |
| changeset 12450 | 1162b280700a |
| parent 12360 | 9c156045c8f2 |
| child 12869 | f362c0323d92 |
| permissions | -rw-r--r-- |
| wenzelm@12115 | 1 |
(* Title: HOL/ex/ROOT.ML |
| wenzelm@12115 | 2 |
ID: $Id$ |
| wenzelm@11586 | 3 |
|
| wenzelm@12115 | 4 |
Miscellaneous examples for Higher-Order Logic. |
| wenzelm@12115 | 5 |
*) |
| wenzelm@12115 | 6 |
|
| wenzelm@12360 | 7 |
time_use_thy "Higher_Order_Logic"; |
| wenzelm@12360 | 8 |
|
| wenzelm@12115 | 9 |
time_use_thy "Recdefs"; |
| wenzelm@12115 | 10 |
time_use_thy "Primrec"; |
| wenzelm@12276 | 11 |
time_use_thy "Locales"; |
| wenzelm@12115 | 12 |
time_use_thy "Records"; |
| wenzelm@12115 | 13 |
time_use_thy "MonoidGroup"; |
| wenzelm@12115 | 14 |
time_use_thy "StringEx"; |
| wenzelm@12115 | 15 |
time_use_thy "BinEx"; |
| wenzelm@12115 | 16 |
setmp proofs 2 time_use_thy "Hilbert_Classical"; |
| wenzelm@12115 | 17 |
time_use_thy "Antiquote"; |
| wenzelm@12115 | 18 |
time_use_thy "Multiquote"; |
| wenzelm@12115 | 19 |
time_use_thy "Tuple"; |
| wenzelm@12115 | 20 |
|
| wenzelm@12115 | 21 |
time_use_thy "NatSum"; |
| berghofe@12450 | 22 |
time_use_thy "Intuitionistic"; |
| wenzelm@12115 | 23 |
time_use "cla.ML"; |
| wenzelm@12115 | 24 |
time_use "mesontest.ML"; |
| wenzelm@12115 | 25 |
time_use_thy "mesontest2"; |
| wenzelm@12115 | 26 |
time_use_thy "BT"; |
| wenzelm@12115 | 27 |
time_use_thy "AVL"; |
| wenzelm@12115 | 28 |
time_use_thy "InSort"; |
| wenzelm@12115 | 29 |
time_use_thy "Qsort"; |
| wenzelm@12115 | 30 |
time_use_thy "Puzzle"; |
| wenzelm@12115 | 31 |
|
| wenzelm@12115 | 32 |
time_use_thy "IntRing"; |
| wenzelm@12115 | 33 |
|
| wenzelm@12115 | 34 |
time_use_thy "set"; |
| wenzelm@12115 | 35 |
time_use_thy "MT"; |
| wenzelm@12115 | 36 |
time_use_thy "Tarski"; |
| wenzelm@12115 | 37 |
|
| wenzelm@12115 | 38 |
if_svc_enabled time_use_thy "svc_test"; |