Re: [isabelle] set comprehension with pairs



Peter Lammich wrote:
You probably mean the @{term ...} antiqotation, i.e. from Isar-level:

ML {* @{term "{(x, y). P x y}"} *}

--
  Peter

No, I definitely meant the command "term", though from the documentation, it looks as though the antiquotation "term" should have a similar effect

Regards,

Jeremy






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