src/HOL/IMP/VC.thy
changeset 25641 615aecd485ad
parent 23746 a455e69c31cc
child 26342 0f65fa163304