[isabelle-dev] Script characters in words

[Makarius]

On 06/03/2024 16:36, Tobias Nipkow wrote:
> 
> On 06/03/2024 15:56, Makarius wrote:
>>
>> The Unicode committee has always been a bit of a mess. I guess the problem 
>> is that US-centric mentality has tried to rule over the world's languages, 
>> with limited success.
> 
> Introducing script "𝒜" much later than "ℬ" is a typical US-centric ploy.

Yes. If you want to understand Unicode history, see this detailed exposition:
http://utf8everywhere.org

I was in particular thinking of the original work by Joseph D. Becker that is 
cited early on that webpage. It reads a bit like "16bit should be sufficient" 
for everything". And then they had to omit many mathematical script 
characters, just because they were not widely used at that time.


	Makarius