Mon, 07 Aug 2000 14:34:26 +0200 | kleing | MicroJava structure changed | changeset | files |
Mon, 07 Aug 2000 14:34:03 +0200 | kleing | Invoke instruction gets fully qualified method name (class+name+sig) as | changeset | files |
Mon, 07 Aug 2000 14:32:56 +0200 | kleing | BV and LBV specified in terms of app and step functions | changeset | files |
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 |