isabelle: src/ZF/Constructible/ROOT.ML@c748d11547d8 (annotated)

13245 714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	1	(* Title: ZF/Constructible/ROOT.ML
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	2	ID: $Id$
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	4	Copyright 2002 University of Cambridge
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	5
13543 2b3c7e319d82 completion of the consistency proof for AC paulson parents: 13503 diff changeset	6	Inner Models, Absoluteness and Consistency Proofs
13245 714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	7	*)
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	8
13503 d93f41fe35d2 Relativization and absoluteness for DPow!! paulson parents: 13494 diff changeset	9	use_thy "DPow_absolute";
13543 2b3c7e319d82 completion of the consistency proof for AC paulson parents: 13503 diff changeset	10	use_thy "AC_in_L";
13634 99a593b49b04 Re-organization of Constructible theories paulson parents: 13543 diff changeset	11	use_thy "Rank_Separation";