src/ZF/Constructible/Datatype_absolute.thy
changeset 13505 52a16cb7fefb
parent 13493 5aa68c051725
child 13557 6061d0045409
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
     1.3 @@ -1,3 +1,9 @@
     1.4 +(*  Title:      ZF/Constructible/Datatype_absolute.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 {*Absoluteness Properties for Recursive Datatypes*}
    1.11  
    1.12  theory Datatype_absolute = Formula + WF_absolute: