src/HOL/IMP/HoareT.thy
changeset 45544 c0304794e9e4
parent 45114 fa3715b35370
child 46203 d43ddad41d81