src/ZF/ex/ROOT.ML
author wenzelm
Sun, 08 Jul 2007 19:51:58 +0200
changeset 23655 d2d1138e0ddc
parent 14883 ca000a495448
child 23912 039ae566a4a2
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12192
6ef4ad110e90 removed BT, Data, Enum (see ZF/Induct);
wenzelm
parents: 12088
diff changeset
     1
(*  Title:      ZF/ex/ROOT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1351
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
12192
6ef4ad110e90 removed BT, Data, Enum (see ZF/Induct);
wenzelm
parents: 12088
diff changeset
     6
Executes miscellaneous examples for Zermelo-Fraenkel Set Theory.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
11399
1605aeb98fd5 two Isar tactic scripts
paulson
parents: 11042
diff changeset
     9
time_use_thy "misc";
14883
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 12229
diff changeset
    10
time_use_thy "Ring";		(*abstract algebra*)
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents: 11399
diff changeset
    11
time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
2248
187d001fbe79 Better indentation
paulson
parents: 1793
diff changeset
    12
time_use_thy "Primes";          (*GCD theory*)
9647
e9623f47275b new example ZF/ex/NatSum
paulson
parents: 9000
diff changeset
    13
time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
2248
187d001fbe79 Better indentation
paulson
parents: 1793
diff changeset
    14
time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
187d001fbe79 Better indentation
paulson
parents: 1793
diff changeset
    15
time_use_thy "Limit";           (*Inverse limit construction of domains*)
11399
1605aeb98fd5 two Isar tactic scripts
paulson
parents: 11042
diff changeset
    16
time_use_thy "BinEx";		(*Binary integer arithmetic*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
960
358a19a91d52 Removed exception handlers, as they are now in ZF/Makefile.
lcp
parents: 919
diff changeset
    18
(** CoDatatypes **)
1351
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    19
time_use_thy "LList";
4a960c012383 removed make_chart;
clasohm
parents: 1296
diff changeset
    20
time_use_thy "CoUnit";