src/HOL/IMP/VC.thy
changeset 19641 f1de44e61ec1
parent 18372 2bffdf62fe7f
child 20503 503ac4c5ef91