Re: [isabelle] How to mark up terms and descriptions?



On 18/10/2019 23:58, Wolfgang Jeltsch wrote:
> Hi!
> 
> The Isabelle/Isar Reference Manual says that `\<^descr>` can be used to
> mark up description list items. However, a description list item
> contains two parts: a term and a description. How do you specify what
> the term and what the description is?

You merely let LaTeX do it: \<^descr>[abc] blah

You can see this in the existing documents, e.g. $ISABELLE_HOME/src/Doc/.


	Makarius




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