made LaTeX happy
authorhaftmann
Sat Jun 22 16:23:25 2019 +0200 (4 weeks ago)
changeset 703574d0b789e4e21
parent 70356 4a327c061870
child 70358 a55cfc8566fd
made LaTeX happy
src/HOL/Fields.thy
     1.1 --- a/src/HOL/Fields.thy	Sat Jun 22 07:18:55 2019 +0000
     1.2 +++ b/src/HOL/Fields.thy	Sat Jun 22 16:23:25 2019 +0200
     1.3 @@ -81,8 +81,8 @@
     1.4  simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
     1.5    \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is
     1.6     really only useful to detect inconsistencies among the premises for subgoals which are
     1.7 -   *not* themselves (in)equalities, because the latter activate
     1.8 -   fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
     1.9 +   \<^emph>\<open>not\<close> themselves (in)equalities, because the latter activate
    1.10 +   \<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the
    1.11     solver all the time rather than add the additional check.\<close>
    1.12  
    1.13  lemmas [arith_split] = nat_diff_split split_min split_max