src/HOL/plain.ML
changeset 41777 1f7cbe39d425
parent 37694 19e8b730ddeb
equal deleted inserted replaced
41776:3bd83302a3c3 41777:1f7cbe39d425