src/HOL/plain.ML
changeset 39774 30cf9d80939e
parent 37694 19e8b730ddeb