Re: [isabelle] Symbols: \<longleftrightarrow> vs. <->
2016-01-21 21:52 GMT+01:00 Makarius <makarius at 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and