diff -r 4805c6333fef -r c7ba70dc49bd Correctness.thy