src/HOL/ex/ROOT.ML
author wenzelm
Sun, 10 Jun 2007 23:48:27 +0200
changeset 23302 919d5c1fe509
parent 23271 3f9ef4bf3f31
child 23454 c54975167be9
permissions -rw-r--r--
disabled theory "Reflected_Presburger" for smlnj (temporarily);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     1
(*  Title:      HOL/ex/ROOT.ML
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     2
    ID:         $Id$
11586
wenzelm
parents: 11445
diff changeset
     3
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     4
Miscellaneous examples for Higher-Order Logic.
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     5
*)
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
     6
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20866
diff changeset
     7
no_document use_thy "Parity";
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20866
diff changeset
     8
no_document use_thy "GCD";
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20866
diff changeset
     9
19438
6d266e266b3f early test of Classpackage, Codegenerator;
wenzelm
parents: 19281
diff changeset
    10
no_document time_use_thy "Classpackage";
23271
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    11
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    12
no_document time_use_thy "Eval";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    13
time_use_thy "Eval_Examples";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    14
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    15
no_document time_use_thy "State_Monad";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    16
no_document time_use_thy "Pretty_Int";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    17
time_use_thy "Random";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    18
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    19
no_document time_use_thy "ExecutableRat";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    20
no_document time_use_thy "EfficientNat";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    21
time_use_thy "Codegenerator_Rat";
21911
e29bcab0c81c added OCaml code generation (without dictionaries)
haftmann
parents: 21256
diff changeset
    22
no_document time_use_thy "Codegenerator";
19438
6d266e266b3f early test of Classpackage, Codegenerator;
wenzelm
parents: 19281
diff changeset
    23
12360
9c156045c8f2 added Higher_Order_Logic.thy;
wenzelm
parents: 12276
diff changeset
    24
time_use_thy "Higher_Order_Logic";
19085
a1a251b297dd added ex/Abstract_NAT.thy;
wenzelm
parents: 19022
diff changeset
    25
time_use_thy "Abstract_NAT";
19997
fe69952f09f6 added ex/Guess.thy;
wenzelm
parents: 19832
diff changeset
    26
time_use_thy "Guess";
22140
0d49078c28bd added HOL/ex/Binary.thy;
wenzelm
parents: 22067
diff changeset
    27
time_use_thy "Binary";
12360
9c156045c8f2 added Higher_Order_Logic.thy;
wenzelm
parents: 12276
diff changeset
    28
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    29
time_use_thy "Recdefs";
22167
c3afded569ea Included ex/Fundefs.thy in HOL-ex session
krauss
parents: 22140
diff changeset
    30
time_use_thy "Fundefs";
14244
f58598341d30 InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents: 14220
diff changeset
    31
time_use_thy "InductiveInvariant_examples";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    32
time_use_thy "Primrec";
12276
7bafe3d6c248 time_use_thy "Locales";
wenzelm
parents: 12274
diff changeset
    33
time_use_thy "Locales";
22657
731622340817 New file for locale regression tests.
ballarin
parents: 22528
diff changeset
    34
time_use_thy "LocaleTest2";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    35
time_use_thy "Records";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    36
time_use_thy "MonoidGroup";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    37
time_use_thy "BinEx";
20866
bc366b4b6ea4 examples for hex and bin numerals
kleing
parents: 20812
diff changeset
    38
time_use_thy "Hex_Bin_Examples";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    39
setmp proofs 2 time_use_thy "Hilbert_Classical";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    40
time_use_thy "Antiquote";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    41
time_use_thy "Multiquote";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    42
20812
cc6b31c2b9a2 reactivated theory PER;
wenzelm
parents: 20597
diff changeset
    43
time_use_thy "PER";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    44
time_use_thy "NatSum";
19022
0e6ec4fd204c * moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents: 18678
diff changeset
    45
time_use_thy "ThreeDivides";
12450
1162b280700a Added example file for intuitionistic logic (taken from FOL).
berghofe
parents: 12360
diff changeset
    46
time_use_thy "Intuitionistic";
14220
4dc132902672 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
paulson
parents: 13880
diff changeset
    47
time_use_thy "Classical";
15871
e524119dbf19 *** empty log message ***
bauerg
parents: 15037
diff changeset
    48
time_use_thy "CTL";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    49
time_use_thy "mesontest2";
23193
1f2d94b6a8ef some tests for arith added
webertj
parents: 23191
diff changeset
    50
time_use_thy "Arith_Examples";
13880
4f7f30f68926 Added examples for Presburger arithmetic.
berghofe
parents: 13200
diff changeset
    51
time_use_thy "PresburgerEx";
23302
919d5c1fe509 disabled theory "Reflected_Presburger" for smlnj (temporarily);
wenzelm
parents: 23271
diff changeset
    52
if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
919d5c1fe509 disabled theory "Reflected_Presburger" for smlnj (temporarily);
wenzelm
parents: 23271
diff changeset
    53
else time_use_thy "Reflected_Presburger";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    54
time_use_thy "BT";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    55
time_use_thy "InSort";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    56
time_use_thy "Qsort";
13200
7618f289c9c1 Added ex/MergeSort
nipkow
parents: 12869
diff changeset
    57
time_use_thy "MergeSort";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    58
time_use_thy "Puzzle";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    59
14603
985eb6708207 Moved ring stuff from ex into Ring_and_Field.
nipkow
parents: 14592
diff changeset
    60
time_use_thy "Lagrange";
23271
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    61
time_use_thy "Groebner_Examples";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    62
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
    63
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
    64
time_use_thy "Commutative_Ring_Complete";
20325
ec52000deb44 added HOL/ex/Reflection;
wenzelm
parents: 19997
diff changeset
    65
time_use_thy "Reflection";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    66
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    67
time_use_thy "set";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    68
time_use_thy "MT";
14569
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    69
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    70
no_document use_thy "FuncSet";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    71
time_use_thy "Tarski";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    72
12869
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents: 12450
diff changeset
    73
time_use_thy "SVC_Oracle";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    74
if_svc_enabled time_use_thy "svc_test";
14459
0a8619367a61 added Refute_Examples.thy
webertj
parents: 14244
diff changeset
    75
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    76
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    77
(* installed:                                                       *)
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18408
diff changeset
    78
try time_use_thy "SAT_Examples";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents: 17505
diff changeset
    79
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    80
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    81
(* installed:                                                       *)
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    82
if getenv "ZCHAFF_HOME" <> "" then
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    83
  time_use_thy "Sudoku"
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    84
else ();
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    85
14462
e6550f190fe9 Refute_Examples added/fixed
webertj
parents: 14459
diff changeset
    86
time_use_thy "Refute_Examples";
14592
dd1a2905ea73 Added theory with examples for quickcheck command.
berghofe
parents: 14569
diff changeset
    87
time_use_thy "Quickcheck_Examples";
19832
1a09f25410da nbe -> NormalForm
nipkow
parents: 19438
diff changeset
    88
no_document time_use_thy "NormalForm";
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents: 14482
diff changeset
    89
14569
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    90
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
    91
time_use_thy "Adder";
14569
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    92
17466
92d36be64b46 Hebrew: HTML.with_charset;
wenzelm
parents: 17413
diff changeset
    93
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
17505
928bd7053d6a Chinese Unicode example;
wenzelm
parents: 17466
diff changeset
    94
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
22999
c1ce129e6f9c Added unification case study (using new function package)
krauss
parents: 22657
diff changeset
    95
c1ce129e6f9c Added unification case study (using new function package)
krauss
parents: 22657
diff changeset
    96
time_use_thy "Unification";