src/HOL/Map.thy
changeset 61799 4cf66f21b764
parent 61069 aefe89038dd2
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Map.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Map.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -275,7 +275,7 @@
     1.4  by (auto simp: map_comp_def split: option.splits)
     1.5  
     1.6  
     1.7 -subsection \<open>@{text "++"}\<close>
     1.8 +subsection \<open>\<open>++\<close>\<close>
     1.9  
    1.10  lemma map_add_empty[simp]: "m ++ empty = m"
    1.11  by(simp add: map_add_def)
    1.12 @@ -640,7 +640,7 @@
    1.13    by (auto simp add: ran_def)
    1.14  
    1.15  
    1.16 -subsection \<open>@{text "map_le"}\<close>
    1.17 +subsection \<open>\<open>map_le\<close>\<close>
    1.18  
    1.19  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
    1.20    by (simp add: map_le_def)