src/HOL/ex/ROOT.ML
author wenzelm
Wed, 29 Aug 2007 20:18:23 +0200
changeset 24478 fb5e3fcfc10c
parent 24195 7d1a16c77f7c
child 24528 e8197c9f1b5c
permissions -rw-r--r--
some simultaneous use_thys;
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
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
     7
no_document use_thys  [
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
     8
  "Parity",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
     9
  "GCD"
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    10
];
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    11
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    12
use_thys [
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    13
  "Higher_Order_Logic",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    14
  "Abstract_NAT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    15
  "Guess",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    16
  "Binary",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    17
  "Recdefs",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    18
  "Fundefs",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    19
  "InductiveInvariant_examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    20
  "Locales",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    21
  "LocaleTest2",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    22
  "Records",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    23
  "MonoidGroup",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    24
  "BinEx",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    25
  "Hex_Bin_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    26
  "Antiquote",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    27
  "Multiquote",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    28
  "PER",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    29
  "NatSum",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    30
  "ThreeDivides",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    31
  "Intuitionistic",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    32
  "CTL",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    33
  "Arith_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    34
  "BT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    35
  "InSort",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    36
  "Qsort",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    37
  "MergeSort",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    38
  "Puzzle",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    39
  "Lagrange",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    40
  "Groebner_Examples",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    41
  "MT",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    42
  "Unification",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    43
  "Commutative_RingEx",
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    44
  "Commutative_Ring_Complete"
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    45
];
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20866
diff changeset
    46
19438
6d266e266b3f early test of Classpackage, Codegenerator;
wenzelm
parents: 19281
diff changeset
    47
no_document time_use_thy "Classpackage";
23271
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    48
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    49
no_document time_use_thy "Eval";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    50
time_use_thy "Eval_Examples";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    51
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    52
no_document time_use_thy "State_Monad";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    53
no_document time_use_thy "Pretty_Int";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    54
time_use_thy "Random";
3f9ef4bf3f31 tuned document;
wenzelm
parents: 23193
diff changeset
    55
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23808
diff changeset
    56
no_document time_use_thy "Executable_Rat";
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23808
diff changeset
    57
no_document time_use_thy "Efficient_Nat";
21911
e29bcab0c81c added OCaml code generation (without dictionaries)
haftmann
parents: 21256
diff changeset
    58
no_document time_use_thy "Codegenerator";
24195
haftmann
parents: 24127
diff changeset
    59
no_document time_use_thy "Codegenerator_Pretty";
19438
6d266e266b3f early test of Classpackage, Codegenerator;
wenzelm
parents: 19281
diff changeset
    60
12360
9c156045c8f2 added Higher_Order_Logic.thy;
wenzelm
parents: 12276
diff changeset
    61
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    62
setmp proofs 2 time_use_thy "Hilbert_Classical";
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    63
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    64
time_use_thy "Primrec";
24478
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    65
time_use_thy "Classical";
fb5e3fcfc10c some simultaneous use_thys;
wenzelm
parents: 24195
diff changeset
    66
time_use_thy "set";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    67
24127
a56b6ed2e49c converted Meson tests to proper theory;
wenzelm
parents: 23854
diff changeset
    68
time_use_thy "Meson_Test";
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23302
diff changeset
    69
time_use_thy "Dense_Linear_Order_Ex";
13880
4f7f30f68926 Added examples for Presburger arithmetic.
berghofe
parents: 13200
diff changeset
    70
time_use_thy "PresburgerEx";
23808
4e4b92e76219 fixed SML/NJ int problem
haftmann
parents: 23502
diff changeset
    71
time_use_thy "Reflected_Presburger";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    72
20325
ec52000deb44 added HOL/ex/Reflection;
wenzelm
parents: 19997
diff changeset
    73
time_use_thy "Reflection";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    74
23502
cc726aa7d66a added NBE
nipkow
parents: 23454
diff changeset
    75
time_use_thy "NBE";
cc726aa7d66a added NBE
nipkow
parents: 23454
diff changeset
    76
14569
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    77
no_document use_thy "FuncSet";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    78
time_use_thy "Tarski";
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    79
12869
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents: 12450
diff changeset
    80
time_use_thy "SVC_Oracle";
12115
d0d41884f787 back to normal;
wenzelm
parents: 12105
diff changeset
    81
if_svc_enabled time_use_thy "svc_test";
14459
0a8619367a61 added Refute_Examples.thy
webertj
parents: 14244
diff changeset
    82
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    83
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    84
(* installed:                                                       *)
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18408
diff changeset
    85
try time_use_thy "SAT_Examples";
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents: 17505
diff changeset
    86
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    87
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    88
(* installed:                                                       *)
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    89
if getenv "ZCHAFF_HOME" <> "" then
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    90
  time_use_thy "Sudoku"
23191
b7f3a30f3d7f MiniSAT mentioned in comment
webertj
parents: 22999
diff changeset
    91
else ();
18408
07da804d1119 ex/Sudoku.thy
webertj
parents: 17783
diff changeset
    92
14462
e6550f190fe9 Refute_Examples added/fixed
webertj
parents: 14459
diff changeset
    93
time_use_thy "Refute_Examples";
14592
dd1a2905ea73 Added theory with examples for quickcheck command.
berghofe
parents: 14569
diff changeset
    94
time_use_thy "Quickcheck_Examples";
19832
1a09f25410da nbe -> NormalForm
nipkow
parents: 19438
diff changeset
    95
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
    96
14569
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    97
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
    98
time_use_thy "Adder";
14569
78b75a9eec01 Added ex/Exceptions.thy
nipkow
parents: 14494
diff changeset
    99
17466
92d36be64b46 Hebrew: HTML.with_charset;
wenzelm
parents: 17413
diff changeset
   100
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
17505
928bd7053d6a Chinese Unicode example;
wenzelm
parents: 17466
diff changeset
   101
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";