src/HOL/plain.ML
changeset 45033 34e5fc15ea02
parent 37694 19e8b730ddeb
equal deleted inserted replaced
45032:5a4d62f9e88d 45033:34e5fc15ea02