src/HOL/intr_elim.ML
changeset 4707 abe6f28a38c1
parent 4089 96fba19bcbe2