src/HOL/intr_elim.ML
changeset 3811 ec27ddb5104c
parent 2688 889a1cbd1aca
child 3978 7e1cfed19d94