src/HOL/plain.ML
changeset 39758 b8a53e3a0ee2
parent 37694 19e8b730ddeb