src/HOL/plain.ML
changeset 49064 bd6cc0b911a1
parent 37694 19e8b730ddeb
equal deleted inserted replaced
49063:f93443defa6c 49064:bd6cc0b911a1