diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Wed May 25 11:50:58 2016 +0200
@@ -33,7 +33,7 @@
   where "metric s = card {v. ~ s v}"
 
 
-text{**We assume that the set of vertices is finite*}
+text\<open>*We assume that the set of vertices is finite\<close>
 axiomatization where
   finite_graph:  "finite (UNIV :: vertex set)"
   
@@ -52,7 +52,7 @@
 
 declare asgt_def [THEN def_act_simp,simp]
 
-text{*All vertex sets are finite*}
+text\<open>All vertex sets are finite\<close>
 declare finite_subset [OF subset_UNIV finite_graph, iff]
 
 declare reach_invariant_def [THEN def_set_simp, simp]