Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Symbols: \<longleftrightarrow> vs. <->


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 12:29 UTC