Mon, 08 Mar 2010 14:42:40 -0800 | huffman | remove unnecessary error handling code | changeset | files |
Mon, 08 Mar 2010 14:12:51 -0800 | huffman | construct fully typed goal in proof of induction rule | changeset | files |
Mon, 08 Mar 2010 13:58:00 -0800 | huffman | don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule | changeset | files |