Theorem about LOG (l2n b ls), and some lemmas about LOG and l2n

The theorem relates the logarithm of the result of l2n to the length of
the list of digits. Now I see LENGTH_l2n says almost the same thing...
delete copy-paste artefact in last commit
add new dropWhile constant to listTheory, and various lemmas
Another theorem characterising LOG (l2n b l)

Uses dropWhile to remove trailing zeroes from l, thereby relaxing the
assumptions on l (to: all digits below b, and at least one non-zero
digit).
fixed an error that Ramana spotted
The ARM model now includes an instruction encoder.

Also, expose the function arm_eval in arm_stepLib.
Update the MIPS model to catch more unpredictable cases.
Update the MIPS step tool to support cases when processor exceptions occur in the branch delay slot.
SYNOPSIS sections end with full stop (dot)
remove munger.o once munger.exe is created
grammar fix
equal spaces around colons