Delete seemingly redundant tools/poly directory (and contents).
Use Const annotations in the TeX pretty-printing backend.

Intention is to allow users to redefine \HOLConst to set their
constant names in something other than the default \texttt.
Make constant annotations appear in more places when pretty-printing.

This affects the TeX selftests, which now see those \HOLConst
annotations (as desired).
The boss/theory_tests can be done with the boss heap.

Move it to after the [poly]bin/hol build-sequence directive to have
this happen.
Remove some unnecessary “magic” invocations in HOLPP.sml

These are a remnant of some ancient black magic in the Moscow ML
implementation.
Preliminary thoughts towards allowing math-mode spacing in HOL TeX.
Extend instruction coverage for the arm_stepLib and arm_progLib tools.

Includes a few fixes.
Remove a debugging "printf" from src/TeX/munger.lex
Provide for special typesetting of type-operators in EmitTeX.

This uses back-end annotations.
Adjust TeX selftest to cope with desired change in bd4bf27aabb209
Update set_fixity documentation to mention set_mapped_fixity.
Improve TeX-mungers' usage messages.
Ensure that FULL_BBLAST_TAC picks up assumptions containing ``word_bit`` terms.
Add tool support for LDM instructions that load to the PC, i.e. those that
perform a branch.
Simplify ordinal.fixpoints_exist proof by using sup_eq_sup theorem.
Define the more efficient osyntax multiplication operation.

This is from the JAR2005 article by Manolios and Vroon.
Abbreviate an ordinal discrete log “constant” and prove it correct.
Prove lemmas 3, 4 and 5 from Manolios and Vroon.
Use testutils in n-bit/selftest.sml
Selftest demonstrating problem of #106.