src/HOL/plain.ML
changeset 48101 1b9796b7ab03
parent 37694 19e8b730ddeb
equal deleted inserted replaced
48100:0122ba071e1a 48101:1b9796b7ab03