src/HOL/IMP/Hoare.thy
changeset 1868 836950047d85
parent 1789 aade046ec6d5
child 2810 c4e16b36bc57