src/HOL/Hoare/Examples.ML
changeset 3718 d78cf498a88c
parent 3372 6e472c8f0011
child 4089 96fba19bcbe2