[isabelle] Lemma pos_mod_bound



Hi,

I noticed that there are two variants of the Lemma pos_mod_bound around,
namely

Divides.pos_mod_bound

and

semiring_numeral_div_class.pos_mod_bound

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?

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.