src/HOL/plain.ML
changeset 41758 a231e6110f9b
parent 37694 19e8b730ddeb