| changeset 69593 | 3dda49e08b9d |
| parent 68460 | b047339bd11c |
| child 71616 | a9de39608b1a |
--- a/src/HOL/Map.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/HOL/Map.thy Fri Jan 04 23:22:53 2019 +0100 @@ -268,7 +268,7 @@ using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def) -subsection \<open>@{const map_option} related\<close> +subsection \<open>\<^const>\<open>map_option\<close> related\<close> lemma map_option_o_empty [simp]: "map_option f \<circ> empty = empty" by (rule ext) simp