src/ZF/Inductive.thy
author lcp
Mon, 19 Dec 1994 13:18:54 +0100
changeset 805 96f51689cdeb
parent 578 efc648d29dd0
child 2870 6d6fd10a9fdc
permissions -rw-r--r--
added true theory dependencies

(*Dummy theory to document dependencies *)

Inductive = Fixedpt + Sum + QPair + "indrule"