Wed, 13 Dec 1995 14:14:06 +0100 renamed parents_of to parents_of_name to avoid name clash with function
clasohm [Wed, 13 Dec 1995 14:14:06 +0100] rev 1403
renamed parents_of to parents_of_name to avoid name clash with function from thm.ML
Mon, 11 Dec 1995 11:24:51 +0100 layout
nipkow [Mon, 11 Dec 1995 11:24:51 +0100] rev 1402
layout
(0) -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip