src/HOL/plain.ML
changeset 41051 2ed1b971fc20
parent 37694 19e8b730ddeb
equal deleted inserted replaced
41050:effbaa323cf0 41051:2ed1b971fc20