more conventional pretty printing; more markup;

tuned white-space;

more specific structure for registration into theory and dependency onto locale

examples for interpretation into target

disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)

handle lambda-lifted problems in Isar construction code

simpler proof through custom summation function

merged

tuned;

tuned;