src/HOL/IMPP/Hoare.thy
changeset 14376 9fe787a90a48
parent 10834 a7897aebbffc
child 17477 ceb42ea2f223