author | Lars Hupel <lars.hupel@mytum.de> |
Thu, 20 Jul 2017 15:41:01 +0200 | |
changeset 66291 | f32968e099d5 |
parent 66289 | 2562f151541c |
child 66292 | 9930f4cf6c7a |
--- a/src/HOL/Library/Finite_Map.thy Thu Jul 20 14:05:29 2017 +0100 +++ b/src/HOL/Library/Finite_Map.thy Thu Jul 20 15:41:01 2017 +0200 @@ -1066,7 +1066,7 @@ unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def by (metis option.collapse option.rel_sel) -lemmas fmap_generic_code = +lemmas [code] = fmrel_code fmran'_alt_def fmdom'_alt_def @@ -1114,8 +1114,6 @@ end -declare fmap_generic_code[code] - subsection \<open>Instances\<close>