# Re: Too narrowly defined: DIVISION SIGN & COLON

From: Hans Aberg <haberg-1_at_telia.com>
Date: Thu, 12 Jul 2012 18:38:07 +0200

On 12 Jul 2012, at 16:06, Julian Bradfield wrote:

> On 2012-07-12, Hans Aberg <haberg-1_at_telia.com> wrote:
>> On 12 Jul 2012, at 12:33, Julian Bradfield wrote:
>>> In practice, no working mathematician is going to use the mathematical
>>> alphanumerical symbols to write maths in (La)TeX, because it's
> ..
>>> the Unicode mathematical symbol model does not match how one uses
>>> mathematical symbols.
>>
>> It is used by proof assistants such as Isabelle, and also in logic.
>> https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
>
> No it isn't.

Yes, I posted before here some example of people using it.

> Isabelle uses (essentially) TeX control sequences
> internally, though it writes them as \<oplus> rather than \oplus .
> A small number of these are mapped to Unicode code points for display
> and input purposes, and that small number does not include any of the
> mathematical alphanumerical symbols block.

Latest version requires STIXFonts to be installed. Some other proof assistants use it.

>> If your only objective is to achieve a rendering for humans to read, TeX is fine, but not if one wants to communicate semantic information on the computer level.
>
> On the contrary, computers are very happy with TeX notation. There are
> several useful mathematical online learning sites (such as, for
> example, Alcumus) which use TeX syntax to interact with the students.

TeX formulas are just for rendering. For example, if you want to have superscript to the left, you have to write \${}^x y\$.

Hans
Received on Thu Jul 12 2012 - 11:42:00 CDT

This archive was generated by hypermail 2.2.0 : Thu Jul 12 2012 - 11:42:01 CDT