Wed, 28 Apr 2004 10:45:35 +0200 comments modified
webertj [Wed, 28 Apr 2004 10:45:35 +0200] rev 14681
comments modified
Mon, 26 Apr 2004 15:01:05 +0200 use Syntax.is_ascii_identifier;
wenzelm [Mon, 26 Apr 2004 15:01:05 +0200] rev 14680
use Syntax.is_ascii_identifier;
Mon, 26 Apr 2004 15:00:20 +0200 added is_ascii_identifier;
wenzelm [Mon, 26 Apr 2004 15:00:20 +0200] rev 14679
added is_ascii_identifier;
Mon, 26 Apr 2004 14:58:54 +0200 clarification of ascii vs. symbolic entities;
wenzelm [Mon, 26 Apr 2004 14:58:54 +0200] rev 14678
clarification of ascii vs. symbolic entities;
Mon, 26 Apr 2004 14:58:29 +0200 tuned presentation;
wenzelm [Mon, 26 Apr 2004 14:58:29 +0200] rev 14677
tuned presentation;
Mon, 26 Apr 2004 14:58:03 +0200 variant: use Symbol.bump_init;
wenzelm [Mon, 26 Apr 2004 14:58:03 +0200] rev 14676
variant: use Symbol.bump_init;
Mon, 26 Apr 2004 14:57:30 +0200 removed obsolete 'undo';
wenzelm [Mon, 26 Apr 2004 14:57:30 +0200] rev 14675
removed obsolete 'undo';
Mon, 26 Apr 2004 14:56:18 +0200 *** empty log message ***
wenzelm [Mon, 26 Apr 2004 14:56:18 +0200] rev 14674
*** empty log message ***
Mon, 26 Apr 2004 14:54:45 +0200 use Syntax.is_identifier;
wenzelm [Mon, 26 Apr 2004 14:54:45 +0200] rev 14673
use Syntax.is_identifier;
Mon, 26 Apr 2004 14:53:29 +0200 use ThmDatabase.is_ml_identifier;
wenzelm [Mon, 26 Apr 2004 14:53:29 +0200] rev 14672
use ThmDatabase.is_ml_identifier;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip