changeset 13505 | 52a16cb7fefb |
parent 13493 | 5aa68c051725 |
child 13557 | 6061d0045409 |
--- a/src/ZF/Constructible/Datatype_absolute.thy Fri Aug 16 12:48:49 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Aug 16 16:41:48 2002 +0200 @@ -1,3 +1,9 @@ +(* Title: ZF/Constructible/Datatype_absolute.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2002 University of Cambridge +*) + header {*Absoluteness Properties for Recursive Datatypes*} theory Datatype_absolute = Formula + WF_absolute: