src/ZF/Datatype.thy
changeset 13328 703de709a64b
parent 12183 c10cea75dd56
child 16417 9bc16273c2d4
equal deleted inserted replaced
13327:be7105a066d3 13328:703de709a64b
     1 (*  Title:      ZF/Datatype.thy
     1 (*  Title:      ZF/Datatype.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 
     5 
     6 (Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
       
     7 *)
     6 *)
       
     7 
       
     8 header{*Datatype and CoDatatype Definitions*}
     8 
     9 
     9 theory Datatype = Inductive + Univ + QUniv
    10 theory Datatype = Inductive + Univ + QUniv
    10   files
    11   files
    11     "Tools/datatype_package.ML"
    12     "Tools/datatype_package.ML"
    12     "Tools/numeral_syntax.ML":  (*belongs to theory Bin*)
    13     "Tools/numeral_syntax.ML":  (*belongs to theory Bin*)