2011-09-06 huffman [Tue, 06 Sep 2011 14:53:51 -0700] rev 44764
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
src/HOL/Complex.thy src/HOL/NSA/NSComplex.thy

2011-09-07 Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 07 Sep 2011 07:59:45 +0900] rev 44763
HOL/Import: Update HOL4 generated files to current Isabelle.
src/HOL/Import/HOL/HOL4Base.thy src/HOL/Import/HOL/HOL4Prob.thy src/HOL/Import/HOL/HOL4Real.thy src/HOL/Import/HOL/HOL4Vec.thy src/HOL/Import/HOL/HOL4Word32.thy src/HOL/Import/HOL/arithmetic.imp src/HOL/Import/HOL/bits.imp src/HOL/Import/HOL/bool.imp src/HOL/Import/HOL/combin.imp src/HOL/Import/HOL/divides.imp src/HOL/Import/HOL/lim.imp src/HOL/Import/HOL/list.imp src/HOL/Import/HOL/num.imp src/HOL/Import/HOL/option.imp src/HOL/Import/HOL/pair.imp src/HOL/Import/HOL/poly.imp src/HOL/Import/HOL/prim_rec.imp src/HOL/Import/HOL/prob_extra.imp src/HOL/Import/HOL/real.imp src/HOL/Import/HOL/realax.imp src/HOL/Import/HOL/rich_list.imp src/HOL/Import/HOL/seq.imp src/HOL/Import/HOL/sum.imp src/HOL/Import/HOL/word32.imp

2011-09-07 wenzelm [Wed, 07 Sep 2011 00:08:09 +0200] rev 44762
tuned proofs;
src/HOL/Statespace/StateFun.thy src/HOL/Word/Examples/WordExamples.thy src/HOL/Word/Word.thy

2011-09-06 huffman [Tue, 06 Sep 2011 13:16:46 -0700] rev 44761
remove some unnecessary simp rules from simpset
src/HOL/Complex.thy

2011-09-06 wenzelm [Tue, 06 Sep 2011 21:56:11 +0200] rev 44760
some Isabelle/jEdit NEWS;
NEWS

2011-09-06 wenzelm [Tue, 06 Sep 2011 21:40:58 +0200] rev 44759
more README;
src/Tools/jEdit/README.html

2011-09-06 wenzelm [Tue, 06 Sep 2011 21:11:12 +0200] rev 44758
merged

2011-09-06 huffman [Tue, 06 Sep 2011 10:30:33 -0700] rev 44757
merged

2011-09-06 huffman [Tue, 06 Sep 2011 10:30:00 -0700] rev 44756
simplify proof of tan_half, removing unused assumptions
src/HOL/Transcendental.thy

2011-09-06 huffman [Tue, 06 Sep 2011 09:56:09 -0700] rev 44755
convert some proofs to Isar-style
src/HOL/Transcendental.thy