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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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