src/ZF/Datatype.thy
changeset 12175 5cf58a1799a7
parent 6070 032babd0120b
child 12183 c10cea75dd56
     1.1 --- a/src/ZF/Datatype.thy	Tue Nov 13 22:20:15 2001 +0100
     1.2 +++ b/src/ZF/Datatype.thy	Tue Nov 13 22:20:51 2001 +0100
     1.3 @@ -1,11 +1,13 @@
     1.4 -(*  Title:      ZF/Datatype
     1.5 +(*  Title:      ZF/Datatype.thy
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1997  University of Cambridge
     1.9  
    1.10 -Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations
    1.11 -
    1.12 -	"Datatype" must be capital to avoid conflicts with ML's "datatype"
    1.13 +(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
    1.14  *)
    1.15  
    1.16 -Datatype = Inductive + Univ + QUniv
    1.17 +theory Datatype = Inductive + Univ + QUniv
    1.18 +  files "Tools/datatype_package.ML":
    1.19 +
    1.20 +end
    1.21 +