src/HOL/Hoare/Examples.thy
changeset 13773 58dc4ab362d0
parent 13737 e564c3d2d174
child 13789 d37f66755f47