Sun, 21 May 2000 14:49:28 +0200 replaced {{ }} by { };
wenzelm [Sun, 21 May 2000 14:49:28 +0200] rev 8902
replaced {{ }} by { };
Sun, 21 May 2000 14:44:01 +0200 cite isabelle-axclass;
wenzelm [Sun, 21 May 2000 14:44:01 +0200] rev 8901
cite isabelle-axclass;
Sun, 21 May 2000 14:42:35 +0200 improved \BG, \EN;
wenzelm [Sun, 21 May 2000 14:42:35 +0200] rev 8900
improved \BG, \EN;
Sun, 21 May 2000 14:37:17 +0200 removed is_type_abbr;
wenzelm [Sun, 21 May 2000 14:37:17 +0200] rev 8899
removed is_type_abbr;
(0) -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip