src/ZF/ROOT.ML

use HOLogic.Not;
export indexify_names;

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

Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.

This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
*)

val banner = "ZF Set Theory (in FOL)";
writeln banner;

eta_contract:=false;

print_depth 1;

(*Add user sections for inductive/datatype definitions*)
use     "~~/src/Pure/section_utils";
use     "thy_syntax";

use_thy "Let";
use_thy "ZF";
use     "Tools/typechk";
use_thy "mono";
use     "ind_syntax";
use     "Tools/cartprod";
use_thy "Fixedpt";
use     "Tools/inductive_package";
use_thy "Inductive";
use     "Tools/induct_tacs";
use     "Tools/primrec_package";
use_thy "QUniv";
use     "Tools/datatype_package";
use_thy "Datatype";
use_thy "InfDatatype";
use_thy "List";

(*Integers & binary integer arithmetic*)
cd "Integ";
use_thy "Bin";
cd "..";

(*the all-in-one theory*)
use_thy "Main";

simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);

print_depth 8;

Goal "True";  (*leave subgoal package empty*)