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.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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.