New prove_case_eq_thm entrypoint for Prim_rec
PDF search did not worked for underscore (_) in Quick Reference.

In text mode LaTeX emulates underscore using horizontal rule, so PDF
search did not work for strings such as "type_abbrev". With T1 font
encoding underscore is always typeset as "_". Other documentation files
are unaffected, for they typeset underscores only with typewriter font.
more hyperlinks in quick reference

Added links to entries that are already documented.
typo: Pre(s)burger
unnecessary abbreviation: theorems as thms.
two .ps and .pdf files added to .gitignore
DESCRIPTION: fixed punctuation, style and typography of 'etc.'