| changeset 67443 | 3abf6a722518 |
| parent 67406 | 23307fd33906 |
| child 67613 | ce654b0e6d69 |
--- a/src/HOL/IMP/Abs_Int3.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/IMP/Abs_Int3.thy Tue Jan 16 09:30:00 2018 +0100 @@ -552,7 +552,7 @@ case 3 thus ?case by(rule m_ivl_widen) next case 4 from 4(2) show ?case by(rule n_ivl_narrow) - \<comment> "note that the first assms is unnecessary for intervals" + \<comment> \<open>note that the first assms is unnecessary for intervals\<close> qed lemma iter_winden_step_ivl_termination: