Since most of the people have objections against using the same (looking)
HTML-representation of two different symbols, I will change it. I think
Mario's proposal using underlining is a good solution. This will result in
the following typesetting definition for the symbol ` _lcm `.
htmldef "_lcm" as "<U>lcm</U>";
althtmldef "_lcm" as "<U>lcm</U>";
latexdef "_lcm" as "\underline{\rm lcm}";
Thanks a lot for your contributions to this discussion.
Alexander
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/3c6498a2-c38c-4333-85da-eae210f4fdffn%40googlegroups.com.
