src/HOL/plain.ML
changeset 50659 0f88591478e6
parent 37694 19e8b730ddeb