| changeset 69593 | 3dda49e08b9d |
| parent 69587 | 53982d5ec0bb |
| child 76213 | e44d86131648 |
--- a/src/ZF/IntDiv.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/ZF/IntDiv.thy Fri Jan 04 23:22:53 2019 +0100 @@ -642,7 +642,7 @@ apply (rule_tac u = "a" and v = "b" in negDivAlg_induct) apply auto apply (simp_all add: quorem_def) - txt\<open>base case: @{term "0$\<le>a$+b"}\<close> + txt\<open>base case: \<^term>\<open>0$\<le>a$+b\<close>\<close> apply (simp add: negDivAlg_eqn) apply (simp add: not_zless_iff_zle [THEN iff_sym]) apply (simp add: int_0_less_mult_iff)