src/HOL/plain.ML
changeset 49811 3fc6b3289c31
parent 37694 19e8b730ddeb