unused;

misc tuning and clarification, notably wrt. flow of context;

isabelle update -u control_cartouches;

removed unused clone of (map o apsnd);
removed unused variant of HOLogic.mk_obj_eq;

added HOLogic.mk_obj_eq convenience and eliminated some clones;

tuned -- use existing Morphism.instantiate_morphism;

tuned signature -- eliminated clones;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

tuned signature -- prefer qualified names;

Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype

useful function

renamed 'fun_rel' to 'rel_fun'

rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user

all_args_conv works also for zero arguments

Lifting: support a type variable as a raw type

restoring Transfer/Lifting context

expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure

lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;

quot_thm_crel

add option_fold

quot_del attribute, it allows us to deregister quotient types

use a quot_map theorem attribute instead of the complicated map attribute

added useful Trueprop_conv

move MRSL to a separate file