Re: [isabelle] code generation for saturated naturals

Hi Peter,

> Thanks for this. I've tidied it up a bit. See the attached.

Thanks a lot.

One further remark: the lemmas nat_mult_min_left etc. are quite generic.
 These should go into a separate prelude section at the beginning of the
theory, from where, after becoming part of the library, they should be
move to appropriate theories in the HOL distribution.

What also comes to my mind is that saturated numbers seem to be a nice
example for complete lattices (with inf = min etc.).  Maybe you still
want to add those instances.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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