author | wenzelm |
Tue, 20 Sep 2005 13:56:34 +0200 | |
changeset 17505 | 928bd7053d6a |
parent 17466 | 92d36be64b46 |
child 17618 | 1330157e156a |
permissions | -rw-r--r-- |
12115 | 1 |
(* Title: HOL/ex/ROOT.ML |
2 |
ID: $Id$ |
|
11586 | 3 |
|
12115 | 4 |
Miscellaneous examples for Higher-Order Logic. |
5 |
*) |
|
6 |
||
12360 | 7 |
time_use_thy "Higher_Order_Logic"; |
8 |
||
12115 | 9 |
time_use_thy "Recdefs"; |
14244
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
14220
diff
changeset
|
10 |
time_use_thy "InductiveInvariant_examples"; |
12115 | 11 |
time_use_thy "Primrec"; |
12276 | 12 |
time_use_thy "Locales"; |
12115 | 13 |
time_use_thy "Records"; |
14 |
time_use_thy "MonoidGroup"; |
|
15 |
time_use_thy "StringEx"; |
|
16 |
time_use_thy "BinEx"; |
|
17 |
setmp proofs 2 time_use_thy "Hilbert_Classical"; |
|
18 |
time_use_thy "Antiquote"; |
|
19 |
time_use_thy "Multiquote"; |
|
20 |
time_use_thy "Tuple"; |
|
21 |
||
22 |
time_use_thy "NatSum"; |
|
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
12360
diff
changeset
|
23 |
time_use_thy "Intuitionistic"; |
14220
4dc132902672
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
paulson
parents:
13880
diff
changeset
|
24 |
time_use_thy "Classical"; |
15871 | 25 |
time_use_thy "CTL"; |
12115 | 26 |
time_use_thy "mesontest2"; |
13880 | 27 |
time_use_thy "PresburgerEx"; |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
15871
diff
changeset
|
28 |
time_use_thy "Reflected_Presburger"; |
12115 | 29 |
time_use_thy "BT"; |
30 |
time_use_thy "InSort"; |
|
31 |
time_use_thy "Qsort"; |
|
13200 | 32 |
time_use_thy "MergeSort"; |
12115 | 33 |
time_use_thy "Puzzle"; |
34 |
||
14603 | 35 |
time_use_thy "Lagrange"; |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
15871
diff
changeset
|
36 |
time_use_thy "Commutative_RingEx"; |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
15871
diff
changeset
|
37 |
time_use_thy "Commutative_Ring_Complete"; |
12115 | 38 |
|
39 |
time_use_thy "set"; |
|
40 |
time_use_thy "MT"; |
|
14569 | 41 |
|
42 |
no_document use_thy "FuncSet"; |
|
12115 | 43 |
time_use_thy "Tarski"; |
44 |
||
12869 | 45 |
time_use_thy "SVC_Oracle"; |
12115 | 46 |
if_svc_enabled time_use_thy "svc_test"; |
14459 | 47 |
|
14462 | 48 |
time_use_thy "Refute_Examples"; |
14592
dd1a2905ea73
Added theory with examples for quickcheck command.
berghofe
parents:
14569
diff
changeset
|
49 |
time_use_thy "Quickcheck_Examples"; |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
14482
diff
changeset
|
50 |
|
14569 | 51 |
no_document use_thy "Word"; |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
14482
diff
changeset
|
52 |
time_use_thy "Adder"; |
14569 | 53 |
|
17466 | 54 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew"; |
17505 | 55 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese"; |