src/ZF/Inductive.thy
author paulson
Wed, 02 Apr 1997 15:25:35 +0200
changeset 2870 6d6fd10a9fdc
parent 805 96f51689cdeb
child 6053 8a1059aa01f0
permissions -rw-r--r--
Now a non-trivial theory so that require_thy can find it

(*Dummy theory to document dependencies *)

Inductive = Fixedpt + Sum + QPair + "indrule" +

end