Patch by Ferruccio that enables \top/\bot for False/True undone.

Patch by Ferruccio that enables \top/\bot for False/True undone.
This needs some rediscussion. In particular:
 1) \top/\bot are also used as the (only?) symbols for bottom/top
    in square lattices. Overloading is not a great idea in this case
    (type vs term).
 2) \bot is also traditionally used as the undefined value. For instance,
    we use it in CerCo for (match ?:\bot in False with []) so that
    you can use/apply \bot just to say that that case is undefined.
    Interpretation can't be used for this because "match"es can't be used
    in interpretations. Thus we use a notation which cannot be overloaded
    and conflicts with Ferruccio's. Is there any other commonly used
    symbol for undefined terms?
 3) True/False are rarely used in statements. Do they really deserve
    a symbol? (maybe they do)

The patch can be re-enabled by re-applying the inverse svn diff of this commit.