src/HOL/base.ML
changeset 47817 5d2d63f4363e
parent 37694 19e8b730ddeb
equal deleted inserted replaced
47812:bb477988edb4 47817:5d2d63f4363e