Re: [isabelle] \<^descr>



On 02/08/16 11:42, Peter Lammich wrote:
> 
> 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?

\<^descr>[name]

See also the sources as examples, e.g. src/Doc/Isar_Ref.


	Makarius





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