src/HOL/Library/AList.thy

--- a/src/HOL/Library/AList.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/AList.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
 *)
 
-section {* Implementation of Association Lists *}
+section \<open>Implementation of Association Lists\<close>
 
 theory AList
 imports Main
@@ -11,14 +11,14 @@
 context
 begin
 
-text {*
+text \<open>
   The operations preserve distinctness of keys and
   function @{term "clearjunk"} distributes over them. Since
   @{term clearjunk} enforces distinctness of keys it can be used
   to establish the invariant, e.g. for inductive proofs.
-*}
+\<close>
 
-subsection {* @{text update} and @{text updates} *}
+subsection \<open>@{text update} and @{text updates}\<close>
 
 qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -68,9 +68,9 @@
 lemma update_last [simp]: "update k v (update k v' al) = update k v al"
   by (induct al) auto
 
-text {* Note that the lists are not necessarily the same:
+text \<open>Note that the lists are not necessarily the same:
         @{term "update k v (update k' v' []) = [(k', v'), (k, v)]"} and
-        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
+        @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.\<close>
 
 lemma update_swap:
   "k \<noteq> k' \<Longrightarrow>
@@ -163,7 +163,7 @@
   by (induct xs arbitrary: ys al) (auto split: list.splits)
 
 
-subsection {* @{text delete} *}
+subsection \<open>@{text delete}\<close>
 
 qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
@@ -215,17 +215,17 @@
   by (simp add: delete_eq)
 
 
-subsection {* @{text update_with_aux} and @{text delete_aux}*}
+subsection \<open>@{text update_with_aux} and @{text delete_aux}\<close>
 
 qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "update_with_aux v k f [] = [(k, f v)]"
 | "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
 
-text {*
+text \<open>
   The above @{term "delete"} traverses all the list even if it has found the key.
   This one does not have to keep going because is assumes the invariant that keys are distinct.
-*}
+\<close>
 qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "delete_aux k [] = []"
@@ -296,7 +296,7 @@
 by(cases ts)(auto split: split_if_asm)
 
 
-subsection {* @{text restrict} *}
+subsection \<open>@{text restrict}\<close>
 
 qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
@@ -380,7 +380,7 @@
   by (induct ps) auto
 
 
-subsection {* @{text clearjunk} *}
+subsection \<open>@{text clearjunk}\<close>
 
 qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -464,7 +464,7 @@
     (simp_all add: clearjunk_delete delete_map assms)
 
 
-subsection {* @{text map_ran} *}
+subsection \<open>@{text map_ran}\<close>
 
 definition map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "map_ran f = map (\<lambda>(k, v). (k, f k v))"
@@ -490,7 +490,7 @@
   by (simp add: map_ran_def split_def clearjunk_map)
 
 
-subsection {* @{text merge} *}
+subsection \<open>@{text merge}\<close>
 
 qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
@@ -558,7 +558,7 @@
   by (simp add: merge_conv')
 
 
-subsection {* @{text compose} *}
+subsection \<open>@{text compose}\<close>
 
 qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
 where
@@ -723,7 +723,7 @@
   by (simp add: compose_conv map_comp_None_iff)
 
 
-subsection {* @{text map_entry} *}
+subsection \<open>@{text map_entry}\<close>
 
 qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
@@ -745,7 +745,7 @@
   using assms by (induct xs) (auto simp add: dom_map_entry)
 
 
-subsection {* @{text map_default} *}
+subsection \<open>@{text map_default}\<close>
 
 fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where