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