--- 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]