src/HOL/plain.ML
changeset 34120 f9920a3ddf50
parent 33615 261abc2e3155
child 37694 19e8b730ddeb
equal deleted inserted replaced
34086:ff8b2ac0134c 34120:f9920a3ddf50