Tue, 12 Oct 2021 20:57:43 +0200 separated commands from annotations to be able to abstract about the latter only
nipkow [Tue, 12 Oct 2021 20:57:43 +0200] rev 74503
separated commands from annotations to be able to abstract about the latter only
Tue, 12 Oct 2021 16:30:43 +0200 prefer standard Term.dest_abs, with minor deviation of generated names;
wenzelm [Tue, 12 Oct 2021 16:30:43 +0200] rev 74502
prefer standard Term.dest_abs, with minor deviation of generated names;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 tip