lib/Tools/fixdots
Thu, 09 Oct 1997 17:45:03 +0200 wenzelm ensure that dots in formulas are followed by non-idents;
less more (0) tip