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