| changeset 65449 | c82e63b11b8b |
| parent 61393 | 8673ec68c798 |
| child 69587 | 53982d5ec0bb |
--- a/src/ZF/Constructible/MetaExists.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Constructible/MetaExists.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section\<open>The meta-existential quantifier\<close> -theory MetaExists imports Main begin +theory MetaExists imports ZF begin text\<open>Allows quantification over any term. Used to quantify over classes. Yields a proposition rather than a FOL formula.\<close>