src/HOL/Hoare/Examples.thy
changeset 30413 c41afa5607be
parent 16796 140f1e0ea846
child 35316 870dfea4f9c0