src/HOL/IMP/VC.ML
changeset 6340 7d5cbd5819a0
parent 5278 a903b66822e2