src/HOL/Hoare/hoare_syntax.ML
changeset 78224 d85d0d41b2bd
parent 74723 f05c73bf5968
child 80636 4041e7c8059d