Fri, 02 Jan 2009 19:29:18 +0100 removed dead code;
wenzelm [Fri, 02 Jan 2009 19:29:18 +0100] rev 29316
removed dead code; proper "_numeral" token markup; proper printing of arguments (higher-order numerals);
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;
Fri, 02 Jan 2009 15:44:33 +0100 added type 'a parser, simplified signature;
wenzelm [Fri, 02 Jan 2009 15:44:33 +0100] rev 29312
added type 'a parser, simplified signature;
Fri, 02 Jan 2009 15:44:33 +0100 added type 'a parser, simplified signature;
wenzelm [Fri, 02 Jan 2009 15:44:33 +0100] rev 29311
added type 'a parser, simplified signature; added internal_command wrapper; tuned;
Fri, 02 Jan 2009 15:44:33 +0100 added type 'a parser, simplified signature;
wenzelm [Fri, 02 Jan 2009 15:44:33 +0100] rev 29310
added type 'a parser, simplified signature; moved properties to value_parse.ML; moved props_text to isar_syn.ML;
Fri, 02 Jan 2009 15:44:32 +0100 added props_text (from outer_parse.ML);
wenzelm [Fri, 02 Jan 2009 15:44:32 +0100] rev 29309
added props_text (from outer_parse.ML);
Fri, 02 Jan 2009 15:44:32 +0100 added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm [Fri, 02 Jan 2009 15:44:32 +0100] rev 29308
added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
Fri, 02 Jan 2009 15:44:32 +0100 added id;
wenzelm [Fri, 02 Jan 2009 15:44:32 +0100] rev 29307
added id; tuned;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip