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