src/HOL/plain.ML
changeset 43735 9b88fd07b912
parent 37694 19e8b730ddeb
equal deleted inserted replaced
43734:ea147bec4f72 43735:9b88fd07b912