diff -r e9ab4ad7bd15 -r 23307fd33906 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -83,14 +83,14 @@
  (let (a1,a2) = inv_plus' a (aval'' e1 S) (aval'' e2 S)
   in inv_aval' e1 a1 (inv_aval' e2 a2 S))"
 
-text{* The test for @{const bot} in the @{const V}-case is important: @{const
+text\<open>The test for @{const bot} in the @{const V}-case is important: @{const
 bot} indicates that a variable has no possible values, i.e.\ that the current
 program point is unreachable. But then the abstract state should collapse to
 @{const None}. Put differently, we maintain the invariant that in an abstract
 state of the form @{term"Some s"}, all variables are mapped to non-@{const
 bot} values. Otherwise the (pointwise) sup of two abstract states, one of
 which contains @{const bot} values, may produce too large a result, thus
-making the analysis less precise. *}
+making the analysis less precise.\<close>
 
 
 fun inv_bval' :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
@@ -108,7 +108,7 @@
   case N thus ?case by simp (metis test_num')
 next
   case (V x)
-  obtain S' where "S = Some S'" and "s : \<gamma>\<^sub>s S'" using `s : \<gamma>\<^sub>o S`
+  obtain S' where "S = Some S'" and "s : \<gamma>\<^sub>s S'" using \<open>s : \<gamma>\<^sub>o S\<close>
     by(auto simp: in_gamma_option_iff)
   moreover hence "s x : \<gamma> (fun S' x)"
     by(simp add: \<gamma>_st_def)
@@ -170,7 +170,7 @@
 proof(simp add: CS_def AI_def)
   assume 1: "pfp (step' \<top>) (bot c) = Some C"
   have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
-  have 2: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C"  --"transfer the pfp'"
+  have 2: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C"  \<comment>"transfer the pfp'"
   proof(rule order_trans)
     show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' \<top> C)" by(rule step_step')
     show "... \<le> \<gamma>\<^sub>c C" by (metis mono_gamma_c[OF pfp'])