Email Gateway (Aug 22 2022 at 12:15): Email Gateway (Aug 22 2022 at 12:15):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
a very small question. I noticed in some theories,
"\<longleftrightarrow>" was replaced by "<->". Is there a specific
reason for this? Should I just prefer "<->" in future?
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 12:15):From: Makarius <makarius@sketis.net>
There were many changes in the opposite direction: old ASCII syntax
replaced by Isabelle symbols. This is also mentioned in NEWS.
Where did you see new emergences of ASCII "<->" instead? It might have
been a mere accident, or an area of non-renovation.
Makarius
Email Gateway (Aug 22 2022 at 12:16):From: "C. Diekmann" <diekmann@in.tum.de>
2016-01-21 21:52 GMT+01:00 Makarius <makarius@sketis.net>:
On Thu, 21 Jan 2016, C. Diekmann wrote:
I noticed in some theories, "\<longleftrightarrow>" was replaced by "<->".
Is there a specific reason for this? Should I just prefer "<->" in future?There were many changes in the opposite direction: old ASCII syntax
replaced by Isabelle symbols. This is also mentioned in NEWS.
Thanks. As described in the NEWS, I will now prefer \<longleftrightarrow>.
Where did you see new emergences of ASCII "<->" instead? It might have been
a mere accident, or an area of non-renovation.
Wrong alarm; sorry. The afp correctly transitioned from <-> to
\<longleftrightarrow>. My private devel repo got slightly out of sync
with the afp and was missing that update. Everything is fine.
Thanks!
Cornelius
Last updated: Nov 21 2024 at 12:39 UTC