src/ZF/Constructible/Datatype_absolute.thy
changeset 13306 6eebcddee32b
parent 13293 09276ee04361
child 13339 0f89104dd377
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 05 17:48:05 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 05 18:33:50 2002 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4 +header {*Absoluteness Properties for Recursive Datatypes*}
     1.5 +
     1.6  theory Datatype_absolute = Formula + WF_absolute:
     1.7  
     1.8