Thu, 04 Mar 2010 17:28:45 +0100 | hoelzl | Added natfloor and floor rules for multiplication and power. | changeset | files |
Thu, 04 Mar 2010 17:09:44 +0100 | hoelzl | Generalized setsum_cases | changeset | files |
Thu, 04 Mar 2010 15:44:06 +0100 | hoelzl | Added vimage_inter_cong | changeset | files |
Thu, 04 Mar 2010 18:18:52 -0800 | huffman | merged | changeset | files |
Thu, 04 Mar 2010 10:01:39 -0800 | huffman | move coinduction-related stuff into function prove_coindunction | changeset | files |
Thu, 04 Mar 2010 08:12:39 -0800 | huffman | add function add_qualified_simp_thm | changeset | files |
Wed, 03 Mar 2010 21:42:42 -0800 | huffman | generate lemma take_below, declare chain_take [simp] | changeset | files |