src/HOL/plain.ML
changeset 50572 b33912e68b84
parent 37694 19e8b730ddeb