[isabelle] Lemma pos_mod_bound
I noticed that there are two variants of the Lemma pos_mod_bound around,
The former takes the shorter name, but the latter is more general
(applicable for 'a :: semiring_numeral_div, not only for int). Apart
from the types, the lemmas are exactly the same.
Can we change the setup so that the shorter name refers to the more
general theorem in future releases?
This archive was generated by a fusion of
Pipermail (Mailman edition) and