src/ZF/ex/Enum.thy
changeset 515 abcc438e7c27
child 810 91c68f74f458
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/Enum.thy	Fri Aug 12 12:28:46 1994 +0200
     1.3 @@ -0,0 +1,24 @@
     1.4 +(*  Title: 	ZF/ex/Enum
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Example of a BIG enumeration type
    1.10 +
    1.11 +Can go up to at least 100 constructors, but it takes nearly 7 minutes...
    1.12 +*)
    1.13 +
    1.14 +Enum = Univ + "Datatype" + 
    1.15 +
    1.16 +consts
    1.17 +  enum :: "i"
    1.18 +
    1.19 +datatype
    1.20 +  "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
    1.21 +         | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
    1.22 +         | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
    1.23 +         | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
    1.24 +         | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
    1.25 +         | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
    1.26 +  
    1.27 +end