licenses: convert license tags to SPDX

misc/pysymbols: Merge some CAmkES functionality for generating apply-style.

This commit resurrects some bitrotted support for generating apply-style proofs
from Python. It is somewhat incomplete and untested, but can serve to make
template proofs much more readable.

misc/pysymbols: Move IsaSymbolsException to a separate file.

misc: Add a Python module for dealing with Isabelle symbols.