Tue, 02 Jul 2002 15:44:04 +0200 print_thms_containing: index variables, refer to local facts as well;
wenzelm [Tue, 02 Jul 2002 15:44:04 +0200] rev 13278
print_thms_containing: index variables, refer to local facts as well;
Tue, 02 Jul 2002 15:41:02 +0200 these_facts: refrain from put_thmss (2nd time!);
wenzelm [Tue, 02 Jul 2002 15:41:02 +0200] rev 13277
these_facts: refrain from put_thmss (2nd time!);
(0) -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip