src/ZF/Constructible/ROOT.ML
author blanchet
Mon, 07 Nov 2011 22:22:01 +0100
changeset 45398 7dbb7b044a11
parent 35762 af3ff2ba4c54
permissions -rw-r--r--
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
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
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
     3
    Copyright   2002  University of Cambridge
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
     4
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 23912
diff changeset
     5
Inner Models, Absoluteness and Consistency Proofs.
13245
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
     6
*)
714f7a423a15 development and tweaks
paulson
parents: 13223
diff changeset
     7
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 13634
diff changeset
     8
use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];