Optimizations for the code which creates 'ctable' (used by isspace and related functions).
Added precondition checks for the isspace, issep, etc. functions in printer.fs; according to the hol-light documentation, these functions are supposed to be used only with strings which are one (1) character in length; however, after adding the preconditions (and some logging), it was found that some parts of the code are passing in longer strings. The preconditions have been wrapped in BUGGY for now, because enabling them means the session crashes almost immediately when attempting to parse a term, but they should be enabled and the call sites fixed at some later time.
Minor formatting and re-organization/de-nesting.
Made a small optimization to 'rightbin' -- instead of calling both 'last' and 'butlast', we call a new function 'extractLast' which returns the same values but only traverses the list once.
Modified the ToString() implementations for 'hol_type' and 'term' so they use sprintf instead of concatenating strings. 'sprintf' is somewhat slower (prior to F# 3.1), but it's simpler to read and the overall performance impact should be negligible.
Disabled logging of messages when charcode is called with strings containing more than one character, because it happens frequently and adds tons of entries to the log.
Merge branch 'master' of github.com:jack-pappas/NHol
Implemented some functions for logging entry/exit of a function.
Changed some uses of logger.Info in theorems.fs to use the new logEntryExitProtected function, and modified some other functions in theorems.fs and equal.fs to use it as well.