author | paulson |
Fri, 03 Jan 1997 15:01:55 +0100 | |
changeset 2469 | b50b8c0eec01 |
parent 1461 | 6bcb44e4d6e5 |
child 4091 | 771b1f6422a8 |
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"; |
2469 | 14 |
by (simp_tac (!simpset addsimps enum.free_iffs) 1); |
0 | 15 |
result(); |
16 |