src/ZF/Constructible/MetaExists.thy
changeset 13505 52a16cb7fefb
parent 13315 685499c73215
child 13634 99a593b49b04
     1.1 --- a/src/ZF/Constructible/MetaExists.thy	Fri Aug 16 12:48:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/MetaExists.thy	Fri Aug 16 16:41:48 2002 +0200
     1.3 @@ -1,3 +1,9 @@
     1.4 +(*  Title:      ZF/Constructible/MetaExists.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   2002  University of Cambridge
     1.8 +*)
     1.9 +
    1.10  header{*The meta-existential quantifier*}
    1.11  
    1.12  theory MetaExists = Main: