Re: [isabelle] Lemma pos_mod_bound

Hi Lars,

> 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?

that is something which could seriously be done.

I guess especially the divisibility matter in HOL-Main is full of rule
duplication which would deserve a systematic cleanup.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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