src/ZF/Inductive.thy
author paulson
Tue, 26 Nov 1996 16:29:30 +0100
changeset 2230 275a5a699ff7
parent 805 96f51689cdeb
child 2870 6d6fd10a9fdc
permissions -rw-r--r--
Structure Bool and value Int.toString needed to replace makestring calls

(*Dummy theory to document dependencies *)

Inductive = Fixedpt + Sum + QPair + "indrule"