src/HOL/Hoare/ROOT.ML
changeset 24772 2b838dfeca1e
parent 24584 01e83ffa6c54
child 35316 870dfea4f9c0