src/HOL/intr_elim.ML
changeset 3884 5423e06b9fe6
parent 2688 889a1cbd1aca
child 3978 7e1cfed19d94