src/HOL/Isar_examples/Hoare.thy
changeset 24323 9aa7b5708eac
parent 22759 e4a3f49eb924
child 24472 943ef707396c