src/ZF/Constructible/ROOT.ML
author wenzelm
Sun, 22 Jul 2007 21:20:56 +0200
changeset 23912 039ae566a4a2
parent 13634 99a593b49b04
child 35762 af3ff2ba4c54
permissions -rw-r--r--
simultaneous use_thys;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 13634
diff changeset
     9
use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];