src/ZF/Constructible/MetaExists.thy
2002-08-16 paulson 2002-08-16 Relativized right up to L satisfies V=L!
2002-07-08 wenzelm 2002-07-08 tuned;
2002-07-08 paulson 2002-07-08 Defining a meta-existential quantifier. Using it to streamline reflection proofs.