So far, it's pretty hard to keep the PDF version going and do some of
the fancier stuff with HTML/CSS; things that pass through fine to HTML
don't pass through to LaTeX as well.

I do hope to put it back someday, see Issue #2

Make all #:tags somewhat consistent

Always use @seclink instead of @secref. The latter is neat, but it's
just too hard to keep track of what the titles are.

Make all @seclinks resolve (in some cases creating stub sections)

Turns out that setting it in the top-level is not enough, so
move it to defs.rkt and use it in ever section