src/HOL/Hoare/ROOT.ML
changeset 15584 3478bb4f93ff
parent 14028 ff6eb32b30a1
child 24104 719fbe4fb77f