isabelle update -u control_cartouches;
apply transfer_prover after folding relator_eq
tuned proofs, to allow unfold_abs_def;
tuning
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle