src/ZF/Constructible/MetaExists.thy

 (*  Title:      ZF/Constructible/MetaExists.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-header{*The meta-existential quantifier*}
+section{*The meta-existential quantifier*}
 
 theory MetaExists imports Main begin
 
 text{*Allows quantification over any term having sort @{text logic}.  Used to
 quantify over classes.  Yields a proposition rather than a FOL formula.*}