src/ZF/Constructible/ROOT.ML

more use of relativized quantifiers
list_closed

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

Inner Models and Absoluteness
*)

use_thy "Reflection";
use_thy "WF_absolute";
use_thy "L_axioms";
use_thy "Datatype_absolute";