| Thu, 08 Sep 2011 09:25:55 +0200 | blanchet | fixed computation of "in_conj" for polymorphic encodings | changeset | files |
| Wed, 07 Sep 2011 22:44:26 -0700 | huffman | add some new lemmas about cis and rcis; | changeset | files |
| Wed, 07 Sep 2011 20:44:39 -0700 | huffman | Complex.thy: move theorems into appropriate subsections | changeset | files |
| Wed, 07 Sep 2011 19:24:28 -0700 | huffman | merged | changeset | files |
| Wed, 07 Sep 2011 17:41:29 -0700 | huffman | remove redundant lemma complex_of_real_minus_one | changeset | files |
| Wed, 07 Sep 2011 18:47:55 -0700 | huffman | simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma | changeset | files |
| Wed, 07 Sep 2011 10:04:07 -0700 | huffman | removed unused lemma sin_cos_squared_add2_mult | changeset | files |