Fri, 02 Jan 2009 16:21:47 +0100 renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm [Fri, 02 Jan 2009 16:21:47 +0100] rev 29315
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
Fri, 02 Jan 2009 16:21:10 +0100 tuned;
wenzelm [Fri, 02 Jan 2009 16:21:10 +0100] rev 29314
tuned;
Fri, 02 Jan 2009 15:44:59 +0100 Isar.command: plain Position.id;
wenzelm [Fri, 02 Jan 2009 15:44:59 +0100] rev 29313
Isar.command: plain Position.id; tuned;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip