src/HOL/IMPP/Hoare.ML
changeset 12395 d6913de7655f
parent 11132 09622301ca07
child 12486 0ed8bdd883e0