src/ZF/ex/Enum.thy
changeset 12194 13909cb72129
parent 12193 b269a927c137
child 12195 ed2893765a08
--- a/src/ZF/ex/Enum.thy	Wed Nov 14 23:22:15 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  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 = Main + 
-
-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