22 Sep
1998
22 Sep
'98
5:23 p.m.
I have made a small change in pl2texi to add the command
@index{...text..}
This is the same as @concept{...text..}, except that it prints in normal font.
Thus, @concept, with its emphasized font, can be used for the first (definitional) appearance of a concept, and @index for other appearances.
Man
--
-----------------------------------------------------------------------------
herme(a)fi.upm.es | Manuel Hermenegildo
herme(a)cs.utexas.edu | Facultad de Informatica
+34-91-336-7435 (Work) | Universidad Politecnica de Madrid
+34-91-352-4819 or 336-7412 (FAX) | 28660-Boadilla del Monte, MADRID
http://www.clip.dia.fi.upm.es/~herme | SPAIN
-----------------------------------------------------------------------------