[isabelle] defining records (development version)

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

Also, if I have

  record inner = 
    fld1 :: nat
    fld2 :: nat

  record outer = 
    fld3 :: inner
    fld4 :: nat

it would be nice if 

  fld3_update (fld1_update (K_record 3)) x

printed more prettily than just the above.  I'm afraid I don't have
any good suggestions as to just what should come out though (HOL4
doesn't do anything nice here either).

Something like 

  x (| fld3.fld1 = 3 |)

would be spiffy, but I don't know if that would work given all the
other constraints on syntax.


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