src/HOL/Isar_examples/Hoare.thy
changeset 23988 aa46577f4f44
parent 22759 e4a3f49eb924
child 24472 943ef707396c