author | wenzelm |
Sat, 27 Oct 2001 00:09:59 +0200 | |
changeset 11963 | a6608d44a46b |
parent 11316 | b4e71bd751e4 |
permissions | -rw-r--r-- |
(* Title: ZF/ex/Enum ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Example of a BIG enumeration type Can go up to at least 100 constructors, but it takes nearly 7 minutes... *) Goal "C00 \\<noteq> C01"; by (Simp_tac 1); result();