Re: [isabelle] Basic IsarToLatex markup completed

On 12/1/2012 11:48 AM, Gottfried Barrow wrote:
Here, I make a pseudo sales speech...

It seems like this would all turn out to be something like one character comments that get implemented like (*...*), other than having to come up with a good way to fit in how they would look.

But I would have eventually settled on using \<^sub> for this, since I've only been using \<^isub>. It pays to get a little information here and there. It would have been a rude awakening after it occurred to me that \<^sub> was the perfect solution all along, and after using the perfect solution for 4 months, the perfect solution then disappeared in the upgrade in 2013.

You can upgrade my psuedo-request and psuedo-sales speech to the real thing.


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