src/HOL/intr_elim.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2