Mon, 03 Jul 1995 13:37:29 +0200 removed debugging output
clasohm [Mon, 03 Jul 1995 13:37:29 +0200] rev 1177
removed debugging output
Mon, 03 Jul 1995 13:08:49 +0200 remove Old_HOL
clasohm [Mon, 03 Jul 1995 13:08:49 +0200] rev 1176
remove Old_HOL
Mon, 03 Jul 1995 13:06:36 +0200 added comments; fixed a bug; reduced memory usage slightly
clasohm [Mon, 03 Jul 1995 13:06:36 +0200] rev 1175
added comments; fixed a bug; reduced memory usage slightly
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip