src/HOL/plain.ML
changeset 43445 270bbbcda059
parent 37694 19e8b730ddeb
equal deleted inserted replaced
43444:f744902b4681 43445:270bbbcda059