src/HOL/plain.ML
changeset 43168 467d5b34e1f5
parent 37694 19e8b730ddeb
equal deleted inserted replaced
43167:839f599bc7ed 43168:467d5b34e1f5