diff -r 2c357e2b8436 -r ade3fc826af3 src/HOL/Boogie/Examples/VCC_Max.thy