author | haftmann |

Sat Jun 22 16:23:25 2019 +0200 (4 weeks ago) | |

changeset 70357 | 4d0b789e4e21 |

parent 70356 | 4a327c061870 |

child 70358 | a55cfc8566fd |

made LaTeX happy

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