src/HOL/Library/Enum.thy

 (*  Title:      HOL/Library/Enum.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Finite types as explicit enumerations *}