isabelle: src/ZF/ex/Enum.ML@b4e71bd751e4 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 515 diff changeset	1	(* Title: ZF/ex/Enum
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 515 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Example of a BIG enumeration type
a5a9c433f639 Initial revision clasohm parents: diff changeset	7
56 2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs lcp parents: 38 diff changeset	8	Can go up to at least 100 constructors, but it takes nearly 7 minutes...
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	9	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6141 diff changeset	11	Goal "C00 \\<noteq> C01";
6141 a6922171b396 removal of the (thm list) argument of mk_cases paulson parents: 5068 diff changeset	12	by (Simp_tac 1);
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	13	result();
a5a9c433f639 Initial revision clasohm parents: diff changeset	14