author | haftmann |
Fri, 02 Jul 2010 17:27:44 +0200 | |
changeset 37692 | 411717732710 |
parent 37691 | bd90378b8171 |
child 37693 | abd5e69bd8cd |
1.1 --- a/src/HOL/Library/Mapping.thy Fri Jul 02 16:50:53 2010 +0200 1.2 +++ b/src/HOL/Library/Mapping.thy Fri Jul 02 17:27:44 2010 +0200 1.3 @@ -278,6 +278,8 @@ 1.4 1.5 subsection {* Code generator setup *} 1.6 1.7 +code_datatype empty update 1.8 + 1.9 instantiation mapping :: (type, type) eq 1.10 begin 1.11