src/HOL/plain.ML
changeset 41537 3837045cc8a1
parent 37694 19e8b730ddeb
equal deleted inserted replaced
41536:47fef6afe756 41537:3837045cc8a1