src/HOL/base.ML
changeset 41910 709c04e7b703
parent 37694 19e8b730ddeb