session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

tuned proofs -- avoid unstructured calculation;

isabelle update_cartouches -c -t;

tuned examples

tuned whitespace

added two 'corec' examples