author | haftmann |
Wed, 15 Apr 2009 15:30:38 +0200 | |
changeset 30924 | c1ed09f3fbfe |
parent 30923 | 2697a1d1d34a |
child 30925 | c38cbc0ac8d1 |
--- 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 *}