void timestamp();
double cpu_so_far();
double time_so_far();
void zeitausgabe(char*,FILE*);
void zeitausgabe_stderr();
void zeitausgabe_stdout();

