src/ZF/intr_elim.thy
author lcp
Mon, 15 Aug 1994 18:07:03 +0200
changeset 520 806d3f00590d
parent 516 1957113f0d7d
permissions -rw-r--r--
ZF/equalities/Sigma_cons: new ZF/equalities/cons_eq: new ZF/equalities.thy: added final newline

(*Dummy theory to document dependencies *)

intr_elim = "add_ind_def"