| author | wenzelm |
| Mon, 02 Dec 1996 10:19:52 +0100 | |
| changeset 2285 | b239c202c91f |
| parent 1461 | 6bcb44e4d6e5 |
| child 2469 | b50b8c0eec01 |
| permissions | -rw-r--r-- |
| 1461 | 1 |
(* Title: ZF/ex/Enum |
| 0 | 2 |
ID: $Id$ |
| 1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| 0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Example of a BIG enumeration type |
|
7 |
||
| 56 | 8 |
Can go up to at least 100 constructors, but it takes nearly 7 minutes... |
| 0 | 9 |
*) |
10 |
||
| 515 | 11 |
open Enum; |
| 0 | 12 |
|
| 515 | 13 |
goal Enum.thy "C00 ~= C01"; |
14 |
by (simp_tac (ZF_ss addsimps enum.free_iffs) 1); |
|
| 0 | 15 |
result(); |
16 |