Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicit code_datatype declaration prevents multiple instantiations later on
authorhaftmann
Fri, 02 Jul 2010 17:27:44 +0200
changeset 37701 411717732710
parent 37700 bd90378b8171
child 37702 abd5e69bd8cd
explicit code_datatype declaration prevents multiple instantiations later on
src/HOL/Library/Mapping.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Mapping.thy	Fri Jul 02 16:50:53 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Jul 02 17:27:44 2010 +0200
@@ -278,6 +278,8 @@
 
 subsection {* Code generator setup *}
 
+code_datatype empty update
+
 instantiation mapping :: (type, type) eq
 begin
isabelle