Re: [isabelle] \<^descr>



On 02/08/16 12:30, Peter Lammich wrote:
> So the structure of this high-level structuring mechanism is only
> established at low-level latex, that happens to interpret the [name]
> (which is just plain text for Isabelle) as optional argument to the
> \item generated by \<^descr>. 
> 
> Regarding the (long-time) goal to output to different formats than latex
> (eg html), I would have expected the (name,text) structure of
> description items to be already established on Isabelle-level.

There is no need to invent a different syntax for Isabelle. It can parse
the [...] notation as in LaTeX.


	Makarius






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