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

Am Samstag, den 19.10.2019, 13:35 +0200 schrieb Makarius:
> 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/.

Hmm, it seems a bit inconsistent that the markup that tells it’s a
description item is part of Isabelle but the markup that distinguishes
the term from the description is not. Are there any plans to introduce
Isabelle markup for the latter as well?

All the best,

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