src/HOL/Isar_examples/Hoare.thy
changeset 23615 40ab945ef5ff
parent 22759 e4a3f49eb924
child 24472 943ef707396c