src/ZF/Inductive.thy
author lcp
Mon Dec 19 13:18:54 1994 +0100 (1994-12-19)
changeset 805 96f51689cdeb
parent 578 efc648d29dd0
child 2870 6d6fd10a9fdc
permissions -rw-r--r--
added true theory dependencies
lcp@578
     1
(*Dummy theory to document dependencies *)
lcp@578
     2
lcp@805
     3
Inductive = Fixedpt + Sum + QPair + "indrule"