summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | skalberg |

Thu, 28 Aug 2003 02:00:16 +0200 | |

changeset 14172 | a872d646bf01 |

parent 14171 | 0cab06e3bbd0 |

child 14173 | a3690aeb79d4 |

Fixed typos.

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