isabelle: src/ZF/ex/Enum.thy@f9eb0f819642 (annotated)

515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	1	(* Title: ZF/ex/Enum
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $Id$
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	4	Copyright 1993 University of Cambridge
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	5
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	6	Example of a BIG enumeration type
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	7
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	8	Can go up to at least 100 constructors, but it takes nearly 7 minutes...
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	9	*)
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	10
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	11	Enum = Univ + "Datatype" +
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	12
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	13	consts
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	14	enum :: "i"
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	15
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	16	datatype
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	17	"enum" = C00 \| C01 \| C02 \| C03 \| C04 \| C05 \| C06 \| C07 \| C08 \| C09
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	18	\| C10 \| C11 \| C12 \| C13 \| C14 \| C15 \| C16 \| C17 \| C18 \| C19
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	19	\| C20 \| C21 \| C22 \| C23 \| C24 \| C25 \| C26 \| C27 \| C28 \| C29
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	20	\| C30 \| C31 \| C32 \| C33 \| C34 \| C35 \| C36 \| C37 \| C38 \| C39
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	21	\| C40 \| C41 \| C42 \| C43 \| C44 \| C45 \| C46 \| C47 \| C48 \| C49
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	22	\| C50 \| C51 \| C52 \| C53 \| C54 \| C55 \| C56 \| C57 \| C58 \| C59
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	23
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	24	end

author	wenzelm
	Wed, 14 Sep 1994 16:11:19 +0200
changeset 613	f9eb0f819642
parent 515	abcc438e7c27
child 810	91c68f74f458
permissions	-rw-r--r--