Thu, 15 Nov 2001 18:16:17 +0100 fixed;
wenzelm [Thu, 15 Nov 2001 18:16:17 +0100] rev 12205
fixed;
Thu, 15 Nov 2001 18:15:58 +0100 Isar version of 'rep_datatype';
wenzelm [Thu, 15 Nov 2001 18:15:58 +0100] rev 12204
Isar version of 'rep_datatype';
Thu, 15 Nov 2001 18:15:32 +0100 avoid handle _;
wenzelm [Thu, 15 Nov 2001 18:15:32 +0100] rev 12203
avoid handle _;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip