| 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