src/HOL/plain.ML
changeset 49963 326f87427719
parent 37694 19e8b730ddeb