src/ZF/Inductive.thy
author paulson
Wed, 23 Apr 1997 10:52:49 +0200
changeset 3015 65778b9d865f
parent 2870 6d6fd10a9fdc
child 6053 8a1059aa01f0
permissions -rw-r--r--
Ran expandshort

(*Dummy theory to document dependencies *)

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

end