src/ZF/InfDatatype.thy
author lcp
Wed, 27 Jul 1994 15:33:42 +0200
changeset 488 52f7447d4f1b
child 516 1957113f0d7d
permissions -rw-r--r--
Addition of infinite branching datatypes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents:
diff changeset
     1
InfDatatype = Datatype + Univ + Cardinal_AC