author | paulson |
Tue, 19 Jan 1999 11:18:11 +0100 | |
changeset 6141 | a6922171b396 |
parent 5068 | fb28eaa07e01 |
child 11316 | b4e71bd751e4 |
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 |
||
5068 | 11 |
Goal "C00 ~= C01"; |
6141 | 12 |
by (Simp_tac 1); |
0 | 13 |
result(); |
14 |