[isabelle] Code Generation for Records



I noticed that the (SML/OCaml) code generator translates Isabelle/HOL
record types into tuple-based data types.  This works reasonably well
(and is understandable, given the internal representation of records in
Isabelle/HOL).  Still, it would be nicer if the code generator instead
used SML/OCaml records where possible.  There is no easy way to achieve
this, is there?

Tjark






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