Re: [isabelle-dev] Notation for not-exists

2016-03-04 Thread Tobias Nipkow
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: (*

Re: [isabelle-dev] Notation for not-exists

2016-03-04 Thread Lawrence Paulson
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.

[isabelle-dev] Notation for not-exists

2016-03-04 Thread Makarius
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