src/HOL/Hoare/ROOT.ML
changeset 23719 ccd9cb15c062
parent 14028 ff6eb32b30a1
child 24104 719fbe4fb77f