# HG changeset patch
# User haftmann
# Date 1561213405 -7200
# Node ID 4d0b789e4e21f5586bfeeebb3f46d9c9d2c13fb0
# Parent  4a327c061870b0d6e0072558e3966abbcf648251
made LaTeX happy

diff -r 4a327c061870 -r 4d0b789e4e21 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Jun 22 07:18:55 2019 +0000
+++ b/src/HOL/Fields.thy	Sat Jun 22 16:23:25 2019 +0200
@@ -81,8 +81,8 @@
 simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
   \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is
    really only useful to detect inconsistencies among the premises for subgoals which are
-   *not* themselves (in)equalities, because the latter activate
-   fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+   \<^emph>\<open>not\<close> themselves (in)equalities, because the latter activate
+   \<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the
    solver all the time rather than add the additional check.\<close>
 
 lemmas [arith_split] = nat_diff_split split_min split_max