more robust, declarative and unsurprising computation of types in the quotient type definition

improve handling of bound type variables (esp. for TFF1)

improved TFF1 output

clarified signature

tuned

tuned

even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);

removed obsolete argument (cf. aa35859c8741);

removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]

extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'

merged

remove unused function

also export DFG formats

always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions

added DFG unsorted support (like in the old days)

gracefully do nothing if the SPASS input file is already in DFG format

added sorted DFG output for coming version of SPASS

specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9

check "sound" flag before doing something unsound...

uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);

tuned;

more accurate class constraints on cancellation simproc patterns

tuned;

tuned Named_Thms: proper binding;

refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;

more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);

uniform Local_Theory.declaration with explicit params;

tuned signature -- refined terminology;

slightly more explicit/syntactic modelling of morphisms;

correct import path