src/HOL/plain.ML
changeset 39905 0bfaaa81fc62
parent 37694 19e8b730ddeb
equal deleted inserted replaced
39904:f9e89d36a31a 39905:0bfaaa81fc62