src/ZF/Inductive.thy
author wenzelm
Mon, 09 Dec 1996 09:03:52 +0100
changeset 2334 00db792beb4e
parent 805 96f51689cdeb
child 2870 6d6fd10a9fdc
permissions -rw-r--r--
added -norc option; error output to stderr;

(*Dummy theory to document dependencies *)

Inductive = Fixedpt + Sum + QPair + "indrule"