src/HOL/UNITY/Simple/Common.thy
changeset 63146 f1ecba0272f9
parent 54863 82acc20ded73
--- a/src/HOL/UNITY/Simple/Common.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Wed May 25 11:50:58 2016 +0200
@@ -97,7 +97,7 @@
     then show ?case by simp
   qed
 next
-  from `n \<in> common`
+  from \<open>n \<in> common\<close>
   show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
     by (simp add: atMost_Int_atLeast)
 qed