Self test was failing.

Remove some Unicode from sources.

improve definition of QbfConv.remove_forall

now use CHANGED_CONV. also some readability tweaks.

Improve HolQbfLib.decide_any

(Progress on #1)

It should now deal with free variables in the input term. Also, fixed a
bug for dealing with a sequence of multiple innermost universal
quantifiers, and in so doing redesigned qbf_prenex_conv substantially.

Also, added another self test and made the self test check for decide_any
check whether an appropriate theorem was produced (rather than assuming
any theorem returned is ok).

Progress on HolQbfLib.decide_any

It should now accept any closed QBF (variables, conjunctions,
disjunctions, implications, quantifiers) as long as all quantified
variables occur somewhere (or maybe even some examples where they
don't).

Improvements to functions in QbfConv welcome.