diff -r b98cd131e2b5 -r 5b5656a63bd6 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Christian Sternagel
 *)
 
-section {* Ad Hoc Overloading *}
+section \<open>Ad Hoc Overloading\<close>
 
 theory Adhoc_Overloading_Examples
 imports
@@ -11,30 +11,30 @@
   "~~/src/HOL/Library/Infinite_Set"
 begin
 
-text {*Adhoc overloading allows to overload a constant depending on
+text \<open>Adhoc overloading allows to overload a constant depending on
 its type. Typically this involves to introduce an uninterpreted
 constant (used for input and output) and then add some variants (used
-internally).*}
+internally).\<close>
 
-subsection {* Plain Ad Hoc Overloading *}
+subsection \<open>Plain Ad Hoc Overloading\<close>
 
-text {*Consider the type of first-order terms.*}
+text \<open>Consider the type of first-order terms.\<close>
 datatype ('a, 'b) "term" =
   Var 'b |
   Fun 'a "('a, 'b) term list"
 
-text {*The set of variables of a term might be computed as follows.*}
+text \<open>The set of variables of a term might be computed as follows.\<close>
 fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
   "term_vars (Var x) = {x}" |
   "term_vars (Fun f ts) = \<Union>set (map term_vars ts)"
 
-text {*However, also for \emph{rules} (i.e., pairs of terms) and term
+text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
 rewrite systems (i.e., sets of rules), the set of variables makes
-sense. Thus we introduce an unspecified constant @{text vars}.*}
+sense. Thus we introduce an unspecified constant @{text vars}.\<close>
 
 consts vars :: "'a \<Rightarrow> 'b set"
 
-text {*Which is then overloaded with variants for terms, rules, and TRSs.*}
+text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
 adhoc_overloading
   vars term_vars
 
@@ -56,20 +56,20 @@
 
 value "vars {(Var 1, Var 0)}"
 
-text {*Sometimes it is necessary to add explicit type constraints
-before a variant can be determined.*}
+text \<open>Sometimes it is necessary to add explicit type constraints
+before a variant can be determined.\<close>
 (*value "vars R" (*has multiple instances*)*)
 value "vars (R :: (('a, 'b) term \<times> ('a, 'b) term) set)"
 
-text {*It is also possible to remove variants.*}
+text \<open>It is also possible to remove variants.\<close>
 no_adhoc_overloading
   vars term_vars rule_vars 
 
 (*value "vars (Var 1)" (*does not have an instance*)*)
 
-text {*As stated earlier, the overloaded constant is only used for
+text \<open>As stated earlier, the overloaded constant is only used for
 input and output. Internally, always a variant is used, as can be
-observed by the configuration option @{text show_variants}.*}
+observed by the configuration option @{text show_variants}.\<close>
 
 adhoc_overloading
   vars term_vars
@@ -79,10 +79,10 @@
 term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*)
 
 
-subsection {* Adhoc Overloading inside Locales *}
+subsection \<open>Adhoc Overloading inside Locales\<close>
 
-text {*As example we use permutations that are parametrized over an
-atom type @{typ "'a"}.*}
+text \<open>As example we use permutations that are parametrized over an
+atom type @{typ "'a"}.\<close>
 
 definition perms :: "('a \<Rightarrow> 'a) set" where
   "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
@@ -90,7 +90,7 @@
 typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
   by standard (auto simp: perms_def)
 
-text {*First we need some auxiliary lemmas.*}
+text \<open>First we need some auxiliary lemmas.\<close>
 lemma permsI [Pure.intro]:
   assumes "bij f" and "MOST x. f x = x"
   shows "f \<in> perms"
@@ -170,16 +170,16 @@
   Rep_perm_uminus
 
 
-section {* Permutation Types *}
+section \<open>Permutation Types\<close>
 
-text {*We want to be able to apply permutations to arbitrary types. To
+text \<open>We want to be able to apply permutations to arbitrary types. To
 this end we introduce a constant @{text PERMUTE} together with
-convenient infix syntax.*}
+convenient infix syntax.\<close>
 
 consts PERMUTE :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b" (infixr "\<bullet>" 75)
 
-text {*Then we add a locale for types @{typ 'b} that support
-appliciation of permutations.*}
+text \<open>Then we add a locale for types @{typ 'b} that support
+appliciation of permutations.\<close>
 locale permute =
   fixes permute :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"
   assumes permute_zero [simp]: "permute 0 x = x"
@@ -191,7 +191,7 @@
 
 end
 
-text {*Permuting atoms.*}
+text \<open>Permuting atoms.\<close>
 definition permute_atom :: "'a perm \<Rightarrow> 'a \<Rightarrow> 'a" where
   "permute_atom p a = (Rep_perm p) a"
 
@@ -201,7 +201,7 @@
 interpretation atom_permute: permute permute_atom
   by standard (simp_all add: permute_atom_def Rep_perm_simps)
 
-text {*Permuting permutations.*}
+text \<open>Permuting permutations.\<close>
 definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
   "permute_perm p q = p + q - p"
 
@@ -215,7 +215,7 @@
   apply (simp only: diff_conv_add_uminus minus_add add.assoc)
   done
 
-text {*Permuting functions.*}
+text \<open>Permuting functions.\<close>
 locale fun_permute =
   dom: permute perm1 + ran: permute perm2
   for perm1 :: "'a perm \<Rightarrow> 'b \<Rightarrow> 'b"