Fri, 16 Dec 1994 17:46:02 +0100 | lcp | Defines ZF theory sections (inductive, datatype) at the start/ | changeset | files |
Fri, 16 Dec 1994 17:44:09 +0100 | lcp | Added Limit_csucc from CardinalArith | changeset | files |
Fri, 16 Dec 1994 17:41:49 +0100 | lcp | Limit_csucc: moved to InfDatatype and proved explicitly in | changeset | files |