src/ZF/intr_elim.thy
author paulson
Mon, 26 May 1997 12:29:55 +0200
changeset 3333 0bbf06e86c06
parent 516 1957113f0d7d
permissions -rw-r--r--
Now checks the name of the function being defined; More de-HOL-ification

(*Dummy theory to document dependencies *)

intr_elim = "add_ind_def"