src/HOL/intr_elim.ML
changeset 3718 d78cf498a88c
parent 2688 889a1cbd1aca
child 3978 7e1cfed19d94