Hi Josef, >If computation is involved, you need more than just passive database. I think I agree with this. With properly automated computations you can throw away all of the AXIOMS and [X]REAL_* and XCMPLX_* series of articles. I _hate_ searching through those articles for lemmas that I know are there, but that I can't find. Freek