src/HOL/intr_elim.thy
changeset 4707 abe6f28a38c1
parent 4084 aa29a521e594