src/HOL/IMPP/Hoare.ML
changeset 13545 fcdbd6cf5f9f
parent 13524 604d0f3622d6
child 13612 55d32e76ef4e