src/ZF/Datatype.thy
author wenzelm
Tue Nov 13 22:20:51 2001 +0100 (2001-11-13)
changeset 12175 5cf58a1799a7
parent 6070 032babd0120b
child 12183 c10cea75dd56
permissions -rw-r--r--
rearranged inductive package for Isar;
     1 (*  Title:      ZF/Datatype.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 (Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
     7 *)
     8 
     9 theory Datatype = Inductive + Univ + QUniv
    10   files "Tools/datatype_package.ML":
    11 
    12 end
    13