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

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/ex/Enum
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
515 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
11354 9b80fe19407f examples files start from Main instead of various ZF theories paulson parents: 1478 diff changeset	11	Enum = Main +
515 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
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 810 diff changeset	14	enum :: i
515 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	paulson
	Thu, 31 May 2001 18:28:23 +0200
changeset 11354	9b80fe19407f
parent 1478	2b8c2a7547ab
permissions	-rw-r--r--