various scripts: use print_function uniformly for python3 compat

misc: Replace inline file merge implementation with isasymbols.

This change means we no longer need to manually update these files when
Isabelle incorporates new unicode symbols. In particular, these translators
will automatically gain support for symbols like "\<longlonglongrightarrow>"
when we move to Isabelle 2016.

misc/filemerge: Remove unnecessary import.

misc: Optimise filemerge scripts.

When streaming a large theory through these scripts, doing string replacements
line-by-line and repeated dictionary lookups become a significant performance
overhead. Relevant observable functionality should be unaffected by this
change.

Import release snapshot.