Sun, 18 May 2008 16:19:48 +0200 proper handling of the return code for the ps-format (fixes a bug)
urbanc [Sun, 18 May 2008 16:19:48 +0200] rev 26954
proper handling of the return code for the ps-format (fixes a bug)
Sun, 18 May 2008 15:28:21 +0200 oops -- pr_graph = Syntax.string_of_term;
wenzelm [Sun, 18 May 2008 15:28:21 +0200] rev 26953
oops -- pr_graph = Syntax.string_of_term; removed dead pr_matrix;
Sun, 18 May 2008 15:04:48 +0200 command 'normal_form': proper context via Variable.auto_fixes;
wenzelm [Sun, 18 May 2008 15:04:48 +0200] rev 26952
command 'normal_form': proper context via Variable.auto_fixes;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip