author | wenzelm |
Sun, 25 Oct 1998 12:33:27 +0100 | |
changeset 5769 | 6a422b22ba02 |
parent 5068 | fb28eaa07e01 |
child 6141 | a6922171b396 |
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 |
|
5068 | 13 |
Goal "C00 ~= C01"; |
4091 | 14 |
by (simp_tac (simpset() addsimps enum.free_iffs) 1); |
0 | 15 |
result(); |
16 |