src/ZF/ex/ROOT.ML
author wenzelm
Mon, 17 Sep 2007 16:36:41 +0200
changeset 24612 d1b315bdb8d7
parent 23912 039ae566a4a2
child 35762 af3ff2ba4c54
permissions -rw-r--r--
avoid direct access to print_mode;

(*  Title:      ZF/ex/ROOT.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Miscellaneous examples for Zermelo-Fraenkel Set Theory.
*)

use_thys [
  "misc",
  "Ring",             (*abstract algebra*)
  "Commutation",      (*abstract Church-Rosser theory*)
  "Primes",           (*GCD theory*)
  "NatSum",           (*Summing integers, squares, cubes, etc.*)
  "Ramsey",           (*Simple form of Ramsey's theorem*)
  "Limit",            (*Inverse limit construction of domains*)
  "BinEx",            (*Binary integer arithmetic*)
  "LList", "CoUnit"   (*CoDatatypes*)
];