src/ZF/Constructible/ROOT.ML
author wenzelm
Wed, 30 Sep 2009 23:28:54 +0200
changeset 32794 7b100d30eb32
parent 23912 039ae566a4a2
child 35762 af3ff2ba4c54
permissions -rw-r--r--
eliminated redundant bindings; schedule_tasks/require_thy: eliminated obsolete tasks_len, which was a leftover from theory-only parallelization;

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

Inner Models, Absoluteness and Consistency Proofs
*)

use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];