wenzelm [Sun, 10 Aug 2008 12:38:25 +0200] rev 27821
read_tyname/const/const_proper: report position;
moved parse_token to syntax.ML;
tuned;
wenzelm [Sun, 10 Aug 2008 12:38:24 +0200] rev 27820
pass position to get_fact;
tuned;
wenzelm [Sun, 10 Aug 2008 12:38:23 +0200] rev 27819
pass token source to typ/term etc.;
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);