src/HOL/Isar_examples/HoareEx.thy
changeset 31757 c1262feb61c7
parent 25706 45d090186bbe