src/HOL/Hoare/hoare_syntax.ML
changeset 79680 0b58e85906a1
parent 74723 f05c73bf5968
child 80636 4041e7c8059d