Re: [isabelle] code generation for saturated naturals


On 08/08/2011, at 4:35 AM, Florian Haftmann wrote:

>> Maybe your Abs_sat' can just be called Sat.
> When going through Dlist a further suggestion came to my mind:
> I have modified the theory further: Abs_sat' is called Sat, and Rep_sat
> nat_of.  Both are operations to be expected to be used in »user space«
> and should therefore carry readable names.

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


Attachment: Saturated.thy
Description: Binary data


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