src/HOL/IMP/VC.thy
changeset 2830 f56e0cac7de9
parent 2810 c4e16b36bc57
child 3842 b55686a7b22c