Tue, 27 Feb 2007 11:10:35 +0100 gensym no longer includes ' or _ in names (trailing _ is bad)
paulson [Tue, 27 Feb 2007 11:10:35 +0100] rev 22368
gensym no longer includes ' or _ in names (trailing _ is bad)
Tue, 27 Feb 2007 00:33:49 +0100 tuned document;
wenzelm [Tue, 27 Feb 2007 00:33:49 +0100] rev 22367
tuned document;
Tue, 27 Feb 2007 00:32:52 +0100 \usepackage{amssymb};
wenzelm [Tue, 27 Feb 2007 00:32:52 +0100] rev 22366
\usepackage{amssymb};
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip