Mon, 07 Aug 2000 10:29:54 +0200 | paulson | instantiated Cancel_Numerals for "nat" in ZF | changeset | files |
Mon, 07 Aug 2000 10:29:04 +0200 | paulson | more cterm operations: mk_implies, list_implies | changeset | files |
Mon, 07 Aug 2000 10:28:32 +0200 | paulson | prove_conv gets an extra argument, so the ZF instantiation can use hyps | changeset | files |