src/HOL/Hoare/hoare_syntax.ML
changeset 56081 72fad75baf7e
parent 55659 4089f6e98ab9
child 59058 a78612c67ec0