src/ZF/InfDatatype.thy
author wenzelm
Wed, 31 Oct 2001 01:21:01 +0100
changeset 11990 c1daefc08eff
parent 516 1957113f0d7d
child 13134 bf37a3049251
permissions -rw-r--r--
use induct_rulify2;

InfDatatype = Datatype + Univ + Finite + Cardinal_AC