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

2016-01-21 21:52 GMT+01:00 Makarius <makarius at>:
> 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.