Mon, 20 Dec 2010 09:48:16 -0800 | huffman | simplify proofs | changeset | files |
Mon, 20 Dec 2010 09:41:55 -0800 | huffman | beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction | changeset | files |