Re: [isabelle] defining records (development version)

Hi Michael,

On Tuesday 14 November 2006 07:24, Michael Norrish wrote:
> It would be nice if the name of the record package's internal K
> combinator (currently "Record.K_record") was available in the
> RecordPackage signature, alongside strings such as updateN and
> others.


>   x (| fld3.fld1 = 3 |)
> would be spiffy, but I don't know if that would work given all the
> other constraints on syntax.

Yes this would be nice. Unfortunately there is a conflict with qualified 
names. If a bright idea and a bag full of time comes along my way I will 
implement some syntax.


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