default instantiation for unit type
authorhaftmann
Wed, 15 Apr 2009 15:30:38 +0200
changeset 30924 c1ed09f3fbfe
parent 30923 2697a1d1d34a
child 30925 c38cbc0ac8d1
default instantiation for unit type
src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Apr 15 15:30:37 2009 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 15 15:30:38 2009 +0200
@@ -84,6 +84,14 @@
 lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
+instantiation unit :: default
+begin
+
+definition "default = ()"
+
+instance ..
+
+end
 
 text {* code generator setup *}