src/ZF/Constructible/ROOT.ML
author wenzelm
Mon Jul 29 00:57:16 2002 +0200 (2002-07-29)
changeset 13428 99e52e78eb65
parent 13339 0f89104dd377
child 13494 1c44289716ae
permissions -rw-r--r--
eliminate open locales and special ML code;
paulson@13245
     1
(*  Title:      ZF/Constructible/ROOT.ML
paulson@13245
     2
    ID:         $Id$
paulson@13245
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13245
     4
    Copyright   2002  University of Cambridge
paulson@13245
     5
paulson@13245
     6
Inner Models and Absoluteness
paulson@13323
     7
paulson@13323
     8
Build using	isatool usedir  -d pdf ZF Constructible
paulson@13245
     9
*)
paulson@13245
    10
paulson@13223
    11
use_thy "Reflection";
paulson@13254
    12
use_thy "WF_absolute";
paulson@13339
    13
use_thy "Rec_Separation";
paulson@13268
    14
use_thy "Datatype_absolute";