src/HOL/base.ML
changeset 46368 ded0390eceae
parent 37694 19e8b730ddeb
equal deleted inserted replaced
46367:723343a03abe 46368:ded0390eceae