Sun, 08 Sep 2013 22:32:47 +0200 | Manuel Eberl | generate elim rules for elimination of function equalities; | changeset | files |
Fri, 13 Sep 2013 07:59:50 +0200 | haftmann | tuned proofs | changeset | files |
Thu, 12 Sep 2013 18:09:56 -0700 | huffman | merged | changeset | files |
Thu, 12 Sep 2013 18:09:17 -0700 | huffman | make 'linear' into a sublocale of 'bounded_linear'; | changeset | files |
Thu, 12 Sep 2013 15:08:46 -0700 | huffman | generalize lemmas | changeset | files |
Thu, 12 Sep 2013 15:08:07 -0700 | huffman | remove unneeded assumption from prime_dvd_power lemmas; | changeset | files |