src/ZF/Inductive.thy
author nipkow
Mon, 13 Jul 1998 16:04:22 +0200
changeset 5133 42a7fe39a63a
parent 2870 6d6fd10a9fdc
child 6053 8a1059aa01f0
permissions -rw-r--r--
swapped condition in update_apply.

(*Dummy theory to document dependencies *)

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

end