src/ZF/Datatype.thy
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 2870 6d6fd10a9fdc
child 6070 032babd0120b
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
paulson@2870
     1
(*  Title:      ZF/Datatype
paulson@2870
     2
    ID:         $Id$
paulson@2870
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2870
     4
    Copyright   1997  University of Cambridge
paulson@2870
     5
paulson@2870
     6
Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations
clasohm@124
     7
paulson@2870
     8
	"Datatype" must be capital to avoid conflicts with ML's "datatype"
paulson@2870
     9
*)
lcp@516
    10
paulson@6053
    11
Datatype = Inductive + Univ + QUniv +
paulson@6053
    12
paulson@6053
    13
setup setup_datatypes
paulson@2870
    14
paulson@2870
    15
end
paulson@2870
    16