src/HOL/plain.ML
changeset 43168 467d5b34e1f5
parent 37694 19e8b730ddeb