src/HOL/Isar_examples/HoareEx.thy
changeset 22871 9ffb43b19ec6
parent 21226 a607ae87ee81
child 25706 45d090186bbe