Thu, 24 Nov 1994 00:33:13 +0100 | lcp | moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML | changeset | files |
Thu, 24 Nov 1994 00:32:43 +0100 | lcp | moved version of Cantors theorem to ZF/Perm.ML | changeset | files |
Thu, 24 Nov 1994 00:32:12 +0100 | lcp | ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually | changeset | files |
Thu, 24 Nov 1994 00:31:41 +0100 | lcp | ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually | changeset | files |
Thu, 24 Nov 1994 00:31:08 +0100 | lcp | updated for new deepen_tac | changeset | files |
Thu, 24 Nov 1994 00:30:35 +0100 | lcp | trivial changes | changeset | files |