| author | webertj |
| Fri, 01 Jun 2007 20:34:12 +0200 | |
| changeset 23191 | b7f3a30f3d7f |
| parent 22999 | c1ce129e6f9c |
| child 23193 | 1f2d94b6a8ef |
| 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@21256 | 7 |
no_document use_thy "Parity"; |
| wenzelm@21256 | 8 |
no_document use_thy "GCD"; |
| wenzelm@21256 | 9 |
|
| wenzelm@19438 | 10 |
no_document time_use_thy "Classpackage"; |
| haftmann@22522 | 11 |
no_document time_use_thy "Eval_examples"; |
| haftmann@22528 | 12 |
no_document time_use_thy "Random"; |
| haftmann@22067 | 13 |
no_document time_use_thy "Codegenerator_Rat"; |
| haftmann@21911 | 14 |
no_document time_use_thy "Codegenerator"; |
| wenzelm@19438 | 15 |
|
| wenzelm@12360 | 16 |
time_use_thy "Higher_Order_Logic"; |
| wenzelm@19085 | 17 |
time_use_thy "Abstract_NAT"; |
| wenzelm@19997 | 18 |
time_use_thy "Guess"; |
| wenzelm@22140 | 19 |
time_use_thy "Binary"; |
| wenzelm@12360 | 20 |
|
| wenzelm@12115 | 21 |
time_use_thy "Recdefs"; |
| krauss@22167 | 22 |
time_use_thy "Fundefs"; |
| paulson@14244 | 23 |
time_use_thy "InductiveInvariant_examples"; |
| wenzelm@12115 | 24 |
time_use_thy "Primrec"; |
| wenzelm@12276 | 25 |
time_use_thy "Locales"; |
| ballarin@22657 | 26 |
time_use_thy "LocaleTest2"; |
| wenzelm@12115 | 27 |
time_use_thy "Records"; |
| wenzelm@12115 | 28 |
time_use_thy "MonoidGroup"; |
| wenzelm@12115 | 29 |
time_use_thy "BinEx"; |
| kleing@20866 | 30 |
time_use_thy "Hex_Bin_Examples"; |
| wenzelm@12115 | 31 |
setmp proofs 2 time_use_thy "Hilbert_Classical"; |
| wenzelm@12115 | 32 |
time_use_thy "Antiquote"; |
| wenzelm@12115 | 33 |
time_use_thy "Multiquote"; |
| wenzelm@12115 | 34 |
|
| wenzelm@20812 | 35 |
time_use_thy "PER"; |
| wenzelm@12115 | 36 |
time_use_thy "NatSum"; |
| kleing@19022 | 37 |
time_use_thy "ThreeDivides"; |
| berghofe@12450 | 38 |
time_use_thy "Intuitionistic"; |
| paulson@14220 | 39 |
time_use_thy "Classical"; |
| bauerg@15871 | 40 |
time_use_thy "CTL"; |
| wenzelm@12115 | 41 |
time_use_thy "mesontest2"; |
| berghofe@13880 | 42 |
time_use_thy "PresburgerEx"; |
| chaieb@17378 | 43 |
time_use_thy "Reflected_Presburger"; |
| wenzelm@12115 | 44 |
time_use_thy "BT"; |
| wenzelm@12115 | 45 |
time_use_thy "InSort"; |
| wenzelm@12115 | 46 |
time_use_thy "Qsort"; |
| nipkow@13200 | 47 |
time_use_thy "MergeSort"; |
| wenzelm@12115 | 48 |
time_use_thy "Puzzle"; |
| wenzelm@12115 | 49 |
|
| nipkow@14603 | 50 |
time_use_thy "Lagrange"; |
| chaieb@17378 | 51 |
time_use_thy "Commutative_RingEx"; |
| chaieb@17378 | 52 |
time_use_thy "Commutative_Ring_Complete"; |
| wenzelm@20325 | 53 |
time_use_thy "Reflection"; |
| wenzelm@12115 | 54 |
|
| wenzelm@12115 | 55 |
time_use_thy "set"; |
| wenzelm@12115 | 56 |
time_use_thy "MT"; |
| nipkow@14569 | 57 |
|
| nipkow@14569 | 58 |
no_document use_thy "FuncSet"; |
| wenzelm@12115 | 59 |
time_use_thy "Tarski"; |
| wenzelm@12115 | 60 |
|
| wenzelm@12869 | 61 |
time_use_thy "SVC_Oracle"; |
| wenzelm@12115 | 62 |
if_svc_enabled time_use_thy "svc_test"; |
| webertj@14459 | 63 |
|
| webertj@23191 | 64 |
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *) |
| webertj@23191 | 65 |
(* installed: *) |
| wenzelm@18678 | 66 |
try time_use_thy "SAT_Examples"; |
| webertj@17618 | 67 |
|
| webertj@23191 | 68 |
(* requires zChaff (or some other reasonably fast SAT solver) to be *) |
| webertj@23191 | 69 |
(* installed: *) |
| webertj@18408 | 70 |
if getenv "ZCHAFF_HOME" <> "" then |
| webertj@18408 | 71 |
time_use_thy "Sudoku" |
| webertj@23191 | 72 |
else (); |
| webertj@18408 | 73 |
|
| webertj@14462 | 74 |
time_use_thy "Refute_Examples"; |
| berghofe@14592 | 75 |
time_use_thy "Quickcheck_Examples"; |
| nipkow@19832 | 76 |
no_document time_use_thy "NormalForm"; |
| skalberg@14494 | 77 |
|
| nipkow@14569 | 78 |
no_document use_thy "Word"; |
| skalberg@14494 | 79 |
time_use_thy "Adder"; |
| nipkow@14569 | 80 |
|
| wenzelm@17466 | 81 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew"; |
| wenzelm@17505 | 82 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese"; |
| krauss@22999 | 83 |
|
| krauss@22999 | 84 |
time_use_thy "Unification"; |