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