src/HOL/base.ML
changeset 39432 12d1be8ff862
parent 37694 19e8b730ddeb
equal deleted inserted replaced
39431:f5320aba6750 39432:12d1be8ff862