| changeset 69505 | cc2d676d5395 |
| parent 68778 | 4566bac4517d |
| child 77136 | 5bf9a1b78f93 |
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Wed Dec 26 16:07:28 2018 +0100 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy Wed Dec 26 16:25:20 2018 +0100 @@ -405,7 +405,7 @@ value "show_acom_opt (AI_ivl test1_ivl)" -text\<open>Better than @{text AI_const}:\<close> +text\<open>Better than \<open>AI_const\<close>:\<close> value "show_acom_opt (AI_ivl test3_const)" value "show_acom_opt (AI_ivl test4_const)" value "show_acom_opt (AI_ivl test6_const)"