20070613 
wenzelm 
20070613 
tuned proofs: avoid implicit prems;

file  diff  annotate 
20070603 
wenzelm 
20070603 
tuned document;

file  diff  annotate 
20061117 
wenzelm 
20061117 
more robust syntax for definition/abbreviation/notation;

file  diff  annotate 
20060911 
wenzelm 
20060911 
induct method: renamed 'fixing' to 'arbitrary';

file  diff  annotate 
20060527 
wenzelm 
20060527 
tuned;

file  diff  annotate 
20060317 
ballarin 
20060317 
Renamed setsum_mult to setsum_right_distrib.

file  diff  annotate 
20060220 
kleing 
20060220 
fixed

file  diff  annotate 
20060219 
kleing 
20060219 
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)
(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)

file  diff  annotate 
20060212 
wenzelm 
20060212 
minor tuning of proofs, notably induct;

file  diff  annotate 
20060212 
kleing 
20060212 
* moved ThreeDivides from Isar_examples to better suited HOL/ex
* moved 2 summation lemmas from ThreeDivides to SetInterval

file  diff  annotate 