wenzelm [Sun, 10 Aug 2008 12:38:22 +0200] rev 27818
added name property operation;
added local_fact;
renamed proposition to prop (again);
wenzelm [Sat, 09 Aug 2008 22:43:59 +0200] rev 27817
renamed ML_Lex.val_of to content_of;
wenzelm [Sat, 09 Aug 2008 22:43:58 +0200] rev 27816
unified Args.T with OuterLex.token, renamed some operations;
moved thm_sel to attrib.ML;
wenzelm [Sat, 09 Aug 2008 22:43:57 +0200] rev 27815
unified Args.T with OuterLex.token;
RESET_VALUE of primitive parsers;
export keyword_with;
renamed keyword_sid to keyword_ident_or_symbolic;
added int (from args.ML);
added enum(1)', and_list(1)' (formerly in args.ML);
removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);
wenzelm [Sat, 09 Aug 2008 22:43:56 +0200] rev 27814
unified Args.T with OuterLex.token;
renamed val_of to content_of;
added InternalValue kind;
added datatype value/slot with static binding (from args.ML);
renamed is_sid to ident_or_symbolic;
wenzelm [Sat, 09 Aug 2008 22:43:55 +0200] rev 27813
unified Args.T with OuterLex.token, renamed some operations;
removed obsolete parse_args (cf. parse);
wenzelm [Sat, 09 Aug 2008 22:43:54 +0200] rev 27812
unified Args.T with OuterLex.token, renamed some operations;
unified version of thm_sel (formerly in args.ML and spec_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:53 +0200] rev 27811
unified Args.T with OuterLex.token;
moved datatype value/slot and basic operations to outer_lex.ML;
removed unused terminator;
removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML);
removed obsolete thm_sel (cf. attrib.ML);
one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:52 +0200] rev 27810
load args.ML later (after outer_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:46 +0200] rev 27809
unified Args.T with OuterLex.token, renamed some operations;