Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/ex/Enum.thy
author clasohm
Sat, 09 Dec 1995 13:36:11 +0100
changeset 1401 0c439768f45c
parent 810 91c68f74f458
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections

(*  Title: 	ZF/ex/Enum
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Example of a BIG enumeration type

Can go up to at least 100 constructors, but it takes nearly 7 minutes...
*)

Enum = Datatype + 

consts
  enum :: i

datatype
  "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
         | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
         | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
         | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
         | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
         | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
  
end
isabelle