| author | paulson | 
| Thu, 15 May 1997 12:54:02 +0200 | |
| changeset 3196 | c522bc46aea7 | 
| parent 2469 | b50b8c0eec01 | 
| 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 |