src/HOL/IMPP/Hoare.ML
changeset 17740 fc385ce6187d
parent 17477 ceb42ea2f223
child 17956 369e2af8ee45