src/HOL/Isar_examples/HoareEx.thy
changeset 12791 ccc0f45ad2c4
parent 11704 3c50a2cd6f00
child 13473 194e8d2cbe0f