src/HOL/base.ML
changeset 48683 eeb4480b5877
parent 37694 19e8b730ddeb