diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Thu May 26 17:51:22 2016 +0200
@@ -6,7 +6,7 @@
 imports Main
 begin
 
-subsection {* The type of distinct lists *}
+subsection \<open>The type of distinct lists\<close>
 
 typedef 'a dlist = "{xs::'a list. distinct xs}"
   morphisms list_of_dlist Abs_dlist
@@ -16,7 +16,7 @@
 
 setup_lifting type_definition_dlist
 
-text {* Fundamental operations: *}
+text \<open>Fundamental operations:\<close>
 
 lift_definition empty :: "'a dlist" is "[]"
 by simp
@@ -33,7 +33,7 @@
 lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.filter
 by simp
 
-text {* Derived operations: *}
+text \<open>Derived operations:\<close>
 
 lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null .
 
@@ -47,7 +47,7 @@
 
 lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto
 
-text {* We can export code: *}
+text \<open>We can export code:\<close>
 
 export_code empty insert remove map filter null member length fold foldr concat in SML