src/HOL/Hoare/Examples.ML
changeset 9914 67e9b7239548
parent 9393 c97111953a66
child 10123 9469c039ff57