1 (* Title: ZF/ex/ROOT.ML |
1 (* Title: ZF/ex/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory. |
6 Miscellaneous examples for Zermelo-Fraenkel Set Theory. |
7 *) |
7 *) |
8 |
8 |
9 time_use_thy "misc"; |
9 use_thys [ |
10 time_use_thy "Ring"; (*abstract algebra*) |
10 "misc", |
11 time_use_thy "Commutation"; (*abstract Church-Rosser theory*) |
11 "Ring", (*abstract algebra*) |
12 time_use_thy "Primes"; (*GCD theory*) |
12 "Commutation", (*abstract Church-Rosser theory*) |
13 time_use_thy "NatSum"; (*Summing integers, squares, cubes, etc.*) |
13 "Primes", (*GCD theory*) |
14 time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) |
14 "NatSum", (*Summing integers, squares, cubes, etc.*) |
15 time_use_thy "Limit"; (*Inverse limit construction of domains*) |
15 "Ramsey", (*Simple form of Ramsey's theorem*) |
16 time_use_thy "BinEx"; (*Binary integer arithmetic*) |
16 "Limit", (*Inverse limit construction of domains*) |
17 |
17 "BinEx", (*Binary integer arithmetic*) |
18 (** CoDatatypes **) |
18 "LList", "CoUnit" (*CoDatatypes*) |
19 time_use_thy "LList"; |
19 ]; |
20 time_use_thy "CoUnit"; |
|