src/Pure/Isar/args.ML
2006-11-23 wenzelm 2006-11-23 renamed Name value to Text, which is *not* a name in terms of morphisms;
2006-11-23 wenzelm 2006-11-23 replaced map_values by morph_values;
2006-10-14 wenzelm 2006-10-14 moved pretty_attribs to attrib.ML;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-30 wenzelm 2006-07-30 added maxidx_values;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-12 wenzelm 2006-07-12 query/bang_colon: separate tokens;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-10 wenzelm 2006-02-10 Context.generic is canonical state of parsers; removed obsolete global/local parsers; tuned interfaces;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-10 wenzelm 2006-01-10 added generic syntax; mk_attribute: generic;
2005-10-28 wenzelm 2005-10-28 syntax for literal facts;
2005-08-18 wenzelm 2005-08-18 removed obsolete Theory.sign_of;
2005-08-16 wenzelm 2005-08-16 added liberal_name;
2005-06-09 wenzelm 2005-06-09 renamed global/local_typ_raw to global/local_typ_abbrev;
2005-05-31 wenzelm 2005-05-31 added symbol scanner;
2005-05-17 wenzelm 2005-05-17 Syntax.read_variable;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** support embedded values and static binding -- via implicit assignment to src tokens (cf. assignable/assign/closure); renamed ident/string/keyword to mk_ident/mk_string/mk_keyword; added mk_name, mk_typ, mk_term, mk_fact, mk_attribute; added type value with map_values etc.; removed name_dummy, added general 'maybe' combinator; added global/local_tyname/const; added pretty_src, pretty_attribs; added thm_sel (from attrib.ML);
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 do *not* export list/list1 -- commas considered special in arg syntax;
2004-05-21 wenzelm 2004-05-21 xxx_typ_raw replace xxx_typ_no_norm forms;
2004-05-19 chaieb 2004-05-19 the function list1 has been exported.
2004-04-19 kleing 2004-04-19 change quote to Library.quote, fixes LaTeX \isarchardoublequote problem.
2004-04-14 wenzelm 2004-04-14 tuned;
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2001-08-21 wenzelm 2001-08-21 tuned error message;
2000-10-04 wenzelm 2000-10-04 added "bracks";
2000-09-19 wenzelm 2000-09-19 added common args keywords;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-07 wenzelm 2000-09-07 avoid handle_error (better msgs);
2000-09-02 wenzelm 2000-09-02 added mode parser;
2000-08-30 wenzelm 2000-08-30 added string_of;
2000-08-04 wenzelm 2000-08-04 added int;
2000-08-03 wenzelm 2000-08-03 typ_no_norm;
2000-06-25 wenzelm 2000-06-25 removed obsolete "{}";
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-05 wenzelm 2000-05-05 GPLed; added colon, parens;
2000-04-12 wenzelm 2000-04-12 Args.name_dummy;
2000-03-21 wenzelm 2000-03-21 goal_spec: [!];
2000-03-20 wenzelm 2000-03-20 goal_spec;
2000-02-22 wenzelm 2000-02-22 tuned syntax wrapper;
2000-02-13 wenzelm 2000-02-13 attrib: keyword_symid; goal_spec;
2000-01-05 wenzelm 2000-01-05 removed pats;
1999-09-21 wenzelm 1999-09-21 added bang_facts;
1999-04-16 wenzelm 1999-04-16 lifted enum; removed list(1); added and_list(1);
1998-11-19 wenzelm 1998-11-19 term_pat vs. prop_pat;
1998-11-17 wenzelm 1998-11-17 removed trace;
1998-11-16 wenzelm 1998-11-16 several args parsers; include positions; misc tuning;
1998-11-09 wenzelm 1998-11-09 Concrete argument syntax (for attributes, methods etc.).