src/HOL/Isar_examples/Hoare.thy
changeset 24403 b7c3ee2ca184
parent 22759 e4a3f49eb924
child 24472 943ef707396c