src/HOL/Hoare/Examples.ML
changeset 5698 2b5d9bdec5af
parent 5655 afd75136b236
child 5983 79e301a6a51b