src/HOL/Hoare/ROOT.ML
changeset 16733 236dfafbeb63
parent 14028 ff6eb32b30a1
child 24104 719fbe4fb77f