src/HOL/intr_elim.ML
changeset 2279 2f337bf81085
parent 2270 d7513875b2b8
child 2414 13df7d6c5c3b