src/ZF/ex/Enum.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/Enum
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Example of a BIG enumeration type
     7 
     8 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
     9 *)
    10 
    11 open Enum;
    12 
    13 goal Enum.thy "C00 ~= C01";
    14 by (simp_tac (ZF_ss addsimps enum.free_iffs) 1);
    15 result();
    16