tuned

tuned

merged

tuned

merged

position constraint for bound dummy -- more PIDE markup;

position constraint for dummy_pattern -- more PIDE markup;

tuned;

tuned signature;

tuned -- less ML compiler warnings;

more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);

more uniform context;

tuned signature;

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;

tuned;