Revert "Implement smarter case pretty-printer. Resolves #165."

This reverts commit 86e201abf6b7591de14e79cfbed0e58bc2d34cd7.

Too many bugs. Will continue development on a separate branch.
add rulename option to LaTeX munger for naming inference rules

Allows the user to provide a string (name) to be passed as the optional
argument to \infer[name]{...} when typesetting using rule or
stackedrule.

Due to the simplistic parsing of the munger's commands and options,
unexpected results are likely if this name contains any special
characters. (Perhaps it should parse them under some encoding for this
option?) The name is wrapped in a new \HOLRuleName command, which
provides a route for customisation.
Add some comments to groundEval.sml
statement of wf_inter improved
inter eq same as lookup eq for sptrees
Update ARM tools to eliminate occurrences of the bitstring operation testbit.
Fixed broken proof

Thanks to Ramana for spotting this.
Test-case for github issue #172

The problem is that the pattern ``x: bool -> bool`` is matching
everything.
Fix bug in pattern-matching within user-pretty-printers.

Closes #172.
Get src/1/selftest.sml to compile under Moscow ML again.

Change in 1ffe317 (new test-case for issue #172) broke compilation
because Moscow ML's handling of record types differs from Poly/ML's.
Add a bit-string rotate operation.
Fixes for the quick reference.

Should work better with more recent versions of LaTeX.
Emacs hol-subgoal-tactic now emulates "suffices_by" as well as "by"

Get the suffices_by effect by using a prefix argument, i.e., by
pressing C-u before invoking it.  Thus, C-u M-h M-s will give you
"suffices_by", and M-h M-s will give you "by" (as before).
Bug-fix for change to hol-subgoal-tactic.

Now behaviour is correct (had to test "raw" prefix argument for nil).
Remove occurrences of testbit from ARM-M0 triples.
Update L3 import.

Extra bit-string shifts are supported.
Add blastLib.BBLAST_PROVE_TAC.
Support x86-64 disassembly for terms of type ``:word8 list``.
Fix header comment.
Fix names used in some exceptions.