src/HOL/plain.ML
changeset 36452 d37c6eed8117
parent 33615 261abc2e3155
child 37694 19e8b730ddeb
equal deleted inserted replaced
36451:ddc965e172c4 36452:d37c6eed8117