src/ZF/InfDatatype.thy
author paulson
Sun, 23 Apr 2000 11:41:45 +0200
changeset 8770 bfab4d4b7516
parent 516 1957113f0d7d
child 13134 bf37a3049251
permissions -rw-r--r--
new, but still slow, proofs using binary numerals

InfDatatype = Datatype + Univ + Finite + Cardinal_AC