[isabelle] selector name in datatype_new causes proof failure



Dear BNF developers,

in Isabelle2014, the datatype_new declaration below results in a proof failure. If I remove the selector name specification bar, the proof succeeds. Is there anything I can do to get the selector names I want?

datatype_new ('t, 'id) foo =
  Foo "('t list ⇒ 't) + 't"
| Bar (bar: 'id)

Andreas




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