thys2/Hoare_abc.thy
changeset 26 1cde7bf45858
parent 25 a5f5b9336007