src/HOL/plain.ML
changeset 50386 d00e2b0ca069
parent 37694 19e8b730ddeb