src/HOL/intr_elim.ML
changeset 3362 0b268cff9344
parent 2688 889a1cbd1aca
child 3978 7e1cfed19d94