src/HOL/Hoare/Examples.ML
changeset 3333 0bbf06e86c06
parent 2031 03a843f0f447
child 3372 6e472c8f0011