author | wenzelm |
Fri, 15 May 1998 11:34:12 +0200 | |
changeset 4932 | c90411dde8e8 |
parent 4091 | 771b1f6422a8 |
child 5068 | fb28eaa07e01 |
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... *) open Enum; goal Enum.thy "C00 ~= C01"; by (simp_tac (simpset() addsimps enum.free_iffs) 1); result();