src/HOL/intr_elim.ML
changeset 4571 6b02fc8a97f6
parent 4089 96fba19bcbe2