src/HOL/IMP/HoareT.thy
changeset 45200 1f1897ac7877
parent 45114 fa3715b35370
child 46203 d43ddad41d81