# HG changeset patch
# User huffman
# Date 1228856005 28800
# Node ID 6cfa380af73b0b5d611b2eacd7e94a05361395ee
# Parent  ef3adebc6d986474379986da66c9d8356c53d672
instantiation option :: (enum) enum

diff -r ef3adebc6d98 -r 6cfa380af73b src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Tue Dec 09 11:49:12 2008 -0800
+++ b/src/HOL/Library/Enum.thy	Tue Dec 09 12:53:25 2008 -0800
@@ -365,4 +365,15 @@
 
 end
 
-end
\ No newline at end of file
+instantiation option :: (enum) enum
+begin
+
+definition
+  "enum = None # map Some enum"
+
+instance by default
+  (auto simp add: enum_all enum_option_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
+
+end
+
+end