author | skalberg |

Thu Aug 28 02:00:16 2003 +0200 (2003-08-28) | |

changeset 14172 | a872d646bf01 |

parent 14171 | 0cab06e3bbd0 |

child 14173 | a3690aeb79d4 |

Fixed typos.

1.1 --- a/NEWS Thu Aug 28 01:56:40 2003 +0200 1.2 +++ b/NEWS Thu Aug 28 02:00:16 2003 +0200 1.3 @@ -10,7 +10,7 @@ 1.4 (\<aa>,...\<zz>,\<AA>,...,\<ZZ>), caligraphic (\<A>...\<Z>), and 1.5 euler (\<a>...\<z>), are now considered normal letters, and can 1.6 therefore be used anywhere where an ASCII letter (a...zA...Z) has 1.7 - until now. Similarily, the symbol digits \<0>...\<9> are now 1.8 + until now. Similarily, the symbol digits \<zero>...\<nine> are now 1.9 considered normal digits. COMPATIBILITY: This obviously changes the 1.10 parsing of some terms, especially where a symbol has been used as a 1.11 binder, say '\<Pi>x. ...', which is now a type error since \<Pi>x