diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Sublist.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -3,13 +3,13 @@
     Author:     Christian Sternagel, JAIST
 *)
 
-section {* List prefixes, suffixes, and homeomorphic embedding *}
+section \<open>List prefixes, suffixes, and homeomorphic embedding\<close>
 
 theory Sublist
 imports Main
 begin
 
-subsection {* Prefix order on lists *}
+subsection \<open>Prefix order on lists\<close>
 
 definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
@@ -38,7 +38,7 @@
   assumes "prefix xs ys"
   obtains z zs where "ys = xs @ z # zs"
 proof -
-  from `prefix xs ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys"
+  from \<open>prefix xs ys\<close> obtain us where "ys = xs @ us" and "xs \<noteq> ys"
     unfolding prefix_def prefixeq_def by blast
   with that show ?thesis by (auto simp add: neq_Nil_conv)
 qed
@@ -53,7 +53,7 @@
   using assms unfolding prefix_def by blast
 
 
-subsection {* Basic properties of prefixes *}
+subsection \<open>Basic properties of prefixes\<close>
 
 theorem Nil_prefixeq [iff]: "prefixeq [] xs"
   by (simp add: prefixeq_def)
@@ -159,7 +159,7 @@
   then show ?thesis using pfx by simp
 next
   case (Cons a as)
-  note c = `ps = a#as`
+  note c = \<open>ps = a#as\<close>
   show ?thesis
   proof (cases ls)
     case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
@@ -195,7 +195,7 @@
 qed
 
 
-subsection {* Parallel lists *}
+subsection \<open>Parallel lists\<close>
 
 definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
   where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
@@ -262,7 +262,7 @@
   unfolding parallel_def by auto
 
 
-subsection {* Suffix order on lists *}
+subsection \<open>Suffix order on lists\<close>
 
 definition suffixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
@@ -363,7 +363,7 @@
   show "suffix\<^sup>=\<^sup>= xs ys"
   proof
     assume "xs \<noteq> ys"
-    with `suffixeq xs ys` show "suffix xs ys"
+    with \<open>suffixeq xs ys\<close> show "suffix xs ys"
       by (auto simp: suffixeq_def suffix_def)
   qed
 next
@@ -426,7 +426,7 @@
   unfolding suffix_def by auto
 
 
-subsection {* Homeomorphic embedding on lists *}
+subsection \<open>Homeomorphic embedding on lists\<close>
 
 inductive list_emb :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
@@ -523,14 +523,14 @@
     case list_emb_Nil show ?case by blast
   next
     case (list_emb_Cons xs ys y)
-    from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
+    from list_emb_ConsD [OF \<open>list_emb P (y#ys) zs\<close>] obtain us v vs
       where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
     then have "list_emb P ys (v#vs)" by blast
     then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
     from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto
   next
     case (list_emb_Cons2 x y xs ys)
-    from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
+    from list_emb_ConsD [OF \<open>list_emb P (y#ys) zs\<close>] obtain us v vs
       where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
     with list_emb_Cons2 have "list_emb P xs vs" by auto
     moreover have "P x v"
@@ -538,7 +538,7 @@
       from zs have "v \<in> set zs" by auto
       moreover have "x \<in> set (x#xs)" and "y \<in> set (y#ys)" by simp_all
       ultimately show ?thesis
-        using `P x y` and `P y v` and list_emb_Cons2
+        using \<open>P x y\<close> and \<open>P y v\<close> and list_emb_Cons2
         by blast
     qed
     ultimately have "list_emb P (x#xs) (v#vs)" by blast
@@ -552,7 +552,7 @@
   using assms by (induct) auto
 
 
-subsection {* Sublists (special case of homeomorphic embedding) *}
+subsection \<open>Sublists (special case of homeomorphic embedding)\<close>
 
 abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "sublisteq xs ys \<equiv> list_emb (op =) xs ys"
@@ -623,7 +623,7 @@
   done
 
 
-subsection {* Appending elements *}
+subsection \<open>Appending elements\<close>
 
 lemma sublisteq_append [simp]:
   "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
@@ -646,7 +646,7 @@
       { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_emb_Cons2 by auto}
       moreover
       { fix us assume "xs=x#us" "ys=[]" then have ?case using list_emb_Cons2(2) by bestsimp }
-      ultimately show ?case using `op = x y` by (auto simp: Cons_eq_append_conv)
+      ultimately show ?case using \<open>op = x y\<close> by (auto simp: Cons_eq_append_conv)
     qed }
   moreover assume ?l
   ultimately show ?r by blast
@@ -661,7 +661,7 @@
   by (metis append_Nil2 list_emb_Nil list_emb_append_mono)
 
 
-subsection {* Relation to standard list operations *}
+subsection \<open>Relation to standard list operations\<close>
 
 lemma sublisteq_map:
   assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"