src/HOL/plain.ML
changeset 49821 d15fe10593ff
parent 37694 19e8b730ddeb