outer_constraints with original variable names, to ensure that argsP is consistent with args

- Equality check on propositions after lookup of theorem now takes type variable renamings into account - Unconstrain theorem after lookup - Improved error messages for application cases

Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.

- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which all type variables have the top sort - Adapted proof_of_term to handle proofs with explicit class membership proofs

merged

merged

corrected printing of characters

corrected implementation

added Scala code setup

tuned code setup