src/HOL/ex/ROOT.ML
author nipkow
Fri, 05 May 2000 12:51:33 +0200
changeset 8797 b55e2354d71e
parent 8569 748a9699f28d
child 8933 de96f2982d2c
permissions -rw-r--r--
Added AVL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1351
diff changeset
     1
(*  Title:      HOL/ex/ROOT
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1351
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     6
Executes miscellaneous examples for Higher-Order Logic. 
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
6349
f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir);
wenzelm
parents: 5866
diff changeset
     9
writeln "Root file for HOL examples";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
4449
wenzelm
parents: 3404
diff changeset
    11
set proof_timing;
3294
4c73b6508f53 New example: ex/Fib
paulson
parents: 3243
diff changeset
    12
5753
wenzelm
parents: 5368
diff changeset
    13
(*some examples of recursive function definitions: the TFL package*)
5124
1ce3cccfacdb stepping stones: Recdef, Main;
wenzelm
parents: 5078
diff changeset
    14
time_use_thy "Recdefs";
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4449
diff changeset
    15
time_use_thy "Primes";
3294
4c73b6508f53 New example: ex/Fib
paulson
parents: 3243
diff changeset
    16
time_use_thy "Fib";
8353
57a163920480 new theory ex/Factorization
paulson
parents: 7304
diff changeset
    17
with_path "../Induct" use_thy "Factorization";
3337
c056d328aa0e Primrec: New example ported from ZF
paulson
parents: 3294
diff changeset
    18
time_use_thy "Primrec";
3294
4c73b6508f53 New example: ex/Fib
paulson
parents: 3243
diff changeset
    19
4c73b6508f53 New example: ex/Fib
paulson
parents: 3243
diff changeset
    20
time_use_thy "NatSum";
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    21
time_use     "cla.ML";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    22
time_use     "meson.ML";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    23
time_use     "mesontest.ML";
8557
fe75fe482566 restored the MESON examples file HOL/ex/mesontest2.ML
paulson
parents: 8353
diff changeset
    24
time_use     "mesontest2.ML";
1174
e57a93d41de0 added mention of new theories BT and Perm
lcp
parents: 1165
diff changeset
    25
time_use_thy "BT";
8797
b55e2354d71e Added AVL
nipkow
parents: 8569
diff changeset
    26
time_use_thy "AVL";
1026
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents: 972
diff changeset
    27
time_use_thy "InSort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents: 972
diff changeset
    28
time_use_thy "Qsort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents: 972
diff changeset
    29
time_use_thy "Puzzle";
3294
4c73b6508f53 New example: ex/Fib
paulson
parents: 3243
diff changeset
    30
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents: 4809
diff changeset
    31
time_use_thy "IntRing";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents: 4809
diff changeset
    32
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    33
time_use     "set.ML";
1026
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
nipkow
parents: 972
diff changeset
    34
time_use_thy "MT";
7085
e5a5f8d23f26 HOL/ex/Tarski: new example by Florian Kammueller
paulson
parents: 6349
diff changeset
    35
time_use_thy "Tarski";
1296
ae31bb7774a7 added calls of init_html and make_chart
clasohm
parents: 1174
diff changeset
    36
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents: 5124
diff changeset
    37
time_use_thy "StringEx";
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents: 5124
diff changeset
    38
time_use_thy "BinEx";
7187
676027b1d770 svc_enabled is now declared as a function
paulson
parents: 7180
diff changeset
    39
7304
94c6f8f07631 if_svc_enabled;
wenzelm
parents: 7187
diff changeset
    40
if_svc_enabled time_use_thy "svc_test";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents: 5124
diff changeset
    41
5753
wenzelm
parents: 5368
diff changeset
    42
(*basic use of extensible records*)
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents: 5124
diff changeset
    43
time_use_thy "MonoidGroup";
5753
wenzelm
parents: 5368
diff changeset
    44
time_use_thy "Points";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents: 5124
diff changeset
    45
5753
wenzelm
parents: 5368
diff changeset
    46
(*groups via locales*)
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents: 5199
diff changeset
    47
time_use_thy "PiSets";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents: 5199
diff changeset
    48
time_use_thy "LocaleGroup";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents: 5199
diff changeset
    49
5753
wenzelm
parents: 5368
diff changeset
    50
(*expressions with quote / antiquote syntax*)
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents: 5250
diff changeset
    51
time_use_thy "Antiquote";
8569
748a9699f28d added HOL/ex/Multiquote.thy;
wenzelm
parents: 8557
diff changeset
    52
time_use_thy "Multiquote";
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents: 5250
diff changeset
    53
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents: 5124
diff changeset
    54
1165
97b2bb5d43c3 renamed CHOL to HOL
clasohm
parents: 1026
diff changeset
    55
writeln "END: Root file for HOL examples";