I think Metamath was available in 1994. (http://us.metamath.org/copyright.html http://us.metamath.org/copyright.html says: The name "Metamath" has been used pub

I think Metamath was available in 1994. (http://us.metamath.org/copyright.html http://us.metamath.org/copyright.html says: The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software.) And even if Devlin wasn't aware of it (or systems like it) back then, what's his excuse now?