src/HOL/base.ML
changeset 46748 8f3ae4d04a2d
parent 37694 19e8b730ddeb
equal deleted inserted replaced
46747:b91628b2522b 46748:8f3ae4d04a2d