src/HOL/intr_elim.ML
changeset 4932 c90411dde8e8
parent 4089 96fba19bcbe2