> On 1 Jul 2015, at 00:57, Makarius <makar...@sketis.net> wrote:
>
> On Tue, 30 Jun 2015, Larry Paulson wrote:
>
>> It is interesting to look at competing systems and note that every one of
>> them appears to be fully committed to a plain ASCII syntax as the only way
>> of writing a formula. I think it may still be premature to abolish having
>> ASCII even as an alternative syntax.
>
> Maybe some HOL4 guy can explain the details. They certainly do have ways to
> use non-ASCII, probably not as pervasive as for Isabelle. (I think they also
> have blue, green, brown variables.)
>
We’ve had support for arbitrary user-chosen UTF8-encoded Unicode symbols since
2008, both in input and output. Emacs has pretty reasonable support for
inputting Unicode if you turn on the TeX-input-method. Our emacs and vim
editing modes further provide keybindings for common symbols (C-S-1 for ∀ is
one more modifier key to press than S-1 (assuming that ! is shift-1)).
We keep material under src/ as pure ASCII, but our examples/ directory is full
of Unicode. E.g.,
val oleast_intro = store_thm(
"oleast_intro",
``∀Q P. (∃α. P α) ∧ (∀α. (∀β. β < α ==> ¬ P β) ∧ P α ==> Q α) ==>
Q ($oleast P)``,
rw[oleast_def] >> SELECT_ELIM_TAC >> conj_tac >-
(match_mp_tac ordlt_WF0 >> metis_tac[]) >>
rw[]);
val ordSUC_def = Define`
ordSUC α = oleast β. α < β
`
I’m not sure why I used the ASCII implication above rather than the Unicode
version, but it does illustrate the way in which the input symbols can be
freely mixed.
Perhaps as a leap of faith, we believe that UTF8-encoded Unicode will be just
as readable as ASCII to the archaeologists of the future. Certainly, in the
present day, it’s nice to be able to read and access sources with tools such as
less, grep etc. and to see stuff like the above.
Michael
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
