diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -1,6 +1,6 @@
 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
 
-section {* A table-based implementation of the reflexive transitive closure *}
+section \<open>A table-based implementation of the reflexive transitive closure\<close>
 
 theory Transitive_Closure_Table
 imports Main
@@ -22,9 +22,9 @@
     then show ?case ..
   next
     case (step x z)
-    from `\<exists>xs. rtrancl_path r z xs y`
+    from \<open>\<exists>xs. rtrancl_path r z xs y\<close>
     obtain xs where "rtrancl_path r z xs y" ..
-    with `r x z` have "rtrancl_path r x (z # xs) y"
+    with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y"
       by (rule rtrancl_path.step)
     then show ?case ..
   qed
@@ -37,7 +37,7 @@
     show ?case by (rule rtranclp.rtrancl_refl)
   next
     case (step x y ys z)
-    from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
+    from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case
       by (rule converse_rtranclp_into_rtranclp)
   qed
 qed
@@ -53,7 +53,7 @@
   case (step x y xs)
   then have "rtrancl_path r y (xs @ ys) z"
     by simp
-  with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
+  with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z"
     by (rule rtrancl_path.step)
   then show ?case by simp
 qed
@@ -83,7 +83,7 @@
       by (rule rtrancl_path.step)
     then have "rtrancl_path r x ((a # as) @ [y]) y"
       by simp
-    then show ?thesis using `rtrancl_path r y ys z`
+    then show ?thesis using \<open>rtrancl_path r y ys z\<close>
       by (rule Cons(2))
   qed
 qed
@@ -96,7 +96,7 @@
   show ?case
   proof (cases "distinct (x # xs)")
     case True
-    with `rtrancl_path r x xs y` show ?thesis by (rule less)
+    with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less)
   next
     case False
     then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
@@ -108,7 +108,7 @@
       case Nil
       with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
         by auto
-      from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
+      from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y"
         by (auto elim: rtrancl_path_appendE)
       from xs have "length cs < length xs" by simp
       then show ?thesis
@@ -117,7 +117,7 @@
       case (Cons d ds)
       with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
         by auto
-      with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
+      with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a"
         and ay: "rtrancl_path r a (bs @ a # cs) y"
         by (auto elim: rtrancl_path_appendE)
       from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
@@ -152,7 +152,7 @@
     by auto
   ultimately have "rtrancl_tab r (x # ys) y z"
     by (rule step)
-  with `x \<notin> set ys` `r x y`
+  with \<open>x \<notin> set ys\<close> \<open>r x y\<close>
   show ?case by (rule rtrancl_tab.step)
 qed