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;

tuned;

syntax translations always depend on context;

updated keywords;

weaker precendence of syntax for big intersection and union on sets

tuned structure

add lemma

bookkeeping and input syntax for exact specification of names of symbols in generated code

use generic data for code symbols for unified "code_printing" syntax for custom serialisations

dedicated module for code symbol data

symbol data covers class relations also

merged

proper internal error, not user error;

tuned;

tuned signature;

tuned;

unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");

tuned signature -- slightly more general operations (cf. term.ML);

re-use Pattern.unify_types, including its trace_unify_fail option;

tuned signature; tuned comments;

improved handling of free variables' types in Isar proofs

pass noninteractive flag -- necessary to run under CASC's "runsolver" program

untabify

more lemmas for sorted_list_of_set