On 04/03/2016 12:34, Makarius wrote:
The Isabelle symbol \ has been there for many years, even with a
standard abbreviation "~?" for the Prover IDE.
A comment in LaTeXsugar.thy from 2005
http://isabelle.in.tum.de/repos/isabelle/file/922e702ae8ca/src/HOL/Library/LaTeXsugar.thy#l23
says: (*
Agree
Larry
> On 4 Mar 2016, at 11:34, Makarius wrote:
>
> I can't imagine anybody using that print mode seriously, so maybe it is time
> to make these syntax variants input-only, as a preparation for removal at a
> later point.
The Isabelle symbol \ has been there for many years, even with a
standard abbreviation "~?" for the Prover IDE.
A comment in LaTeXsugar.thy from 2005
http://isabelle.in.tum.de/repos/isabelle/file/922e702ae8ca/src/HOL/Library/LaTeXsugar.thy#l23
says: (* should become standard syntax once