session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
isabelle update_cartouches -c -t;
more canonical names
tuned headers;
avoid undeclared variables within proofs;
tuned
slightly tuned
Yet another proof of False, this time using the strong case analysis rule.
tuned proofs and comments
tuned proofs
adapted theory name;
polishing of some proofs