src/ZF/Datatype.thy
author paulson
Tue Jul 09 23:05:26 2002 +0200 (2002-07-09)
changeset 13328 703de709a64b
parent 12183 c10cea75dd56
child 16417 9bc16273c2d4
permissions -rw-r--r--
better document preparation
     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 *)
     7 
     8 header{*Datatype and CoDatatype Definitions*}
     9 
    10 theory Datatype = Inductive + Univ + QUniv
    11   files
    12     "Tools/datatype_package.ML"
    13     "Tools/numeral_syntax.ML":  (*belongs to theory Bin*)
    14 
    15 end