[isabelle] HOLCF and records



Hello

Is it possible to define records in HOLCF (Isabelle 2009-1)? 
This code raises an exception:

theory Tst
imports HOLCF
begin

record rec1 =
 f1 :: nat

typ rec1

*** exception TYPE raised (line 311 of "type.ML"): Type variable "?'z" has two distinct sorts
*** At command "typ".

Regards,
Maxim




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