2011-09-05 haftmann [Mon, 05 Sep 2011 19:18:38 +0200] rev 44832
merged

2011-09-05 haftmann [Mon, 05 Sep 2011 07:49:31 +0200] rev 44831
tuned
src/HOL/Finite_Set.thy

2011-09-04 haftmann [Sun, 04 Sep 2011 09:28:15 +0200] rev 44830
tuned
src/HOL/Nominal/nominal_permeq.ML

2011-09-08 blanchet [Thu, 08 Sep 2011 09:25:55 +0200] rev 44829
fixed computation of "in_conj" for polymorphic encodings
src/HOL/Tools/ATP/atp_translate.ML

2011-09-07 huffman [Wed, 07 Sep 2011 22:44:26 -0700] rev 44828
add some new lemmas about cis and rcis;
simplify some proofs;
src/HOL/Complex.thy

2011-09-07 huffman [Wed, 07 Sep 2011 20:44:39 -0700] rev 44827
Complex.thy: move theorems into appropriate subsections
src/HOL/Complex.thy

2011-09-07 huffman [Wed, 07 Sep 2011 19:24:28 -0700] rev 44826
merged
NEWS

2011-09-07 huffman [Wed, 07 Sep 2011 17:41:29 -0700] rev 44825
remove redundant lemma complex_of_real_minus_one
src/HOL/Complex.thy

2011-09-07 huffman [Wed, 07 Sep 2011 18:47:55 -0700] rev 44824
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
src/HOL/Complex.thy src/HOL/NSA/NSComplex.thy

2011-09-07 huffman [Wed, 07 Sep 2011 10:04:07 -0700] rev 44823
removed unused lemma sin_cos_squared_add2_mult
src/HOL/Complex.thy