Re: [isabelle] code generation for saturated naturals



Florian,

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.

cheers
peter

Attachment: Saturated.thy
Description: Binary data


-- 
http://peteg.org/



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