[isabelle] \<^descr>



Hi all,

according to the isar-ref manual, \<^descr> shall be a markdown-like
version for description. However, it is nowhere documented how to
specify the name for the item. Also a quick inspection of the source
code gives no clues.

Any hints?

--
  Peter





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