diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Sublist_Order.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -3,19 +3,19 @@
                 Florian Haftmann, Tobias Nipkow, TU Muenchen
 *)
 
-section {* Sublist Ordering *}
+section \<open>Sublist Ordering\<close>
 
 theory Sublist_Order
 imports Sublist
 begin
 
-text {*
+text \<open>
   This theory defines sublist ordering on lists.
   A list @{text ys} is a sublist of a list @{text xs},
   iff one obtains @{text ys} by erasing some elements from @{text xs}.
-*}
+\<close>
 
-subsection {* Definitions and basic lemmas *}
+subsection \<open>Definitions and basic lemmas\<close>
 
 instantiation list :: (type) ord
 begin