src/Pure/Isar/args.ML
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-09-02 wenzelm 2008-09-02 added binding; thm_name/opt_thm_name: Name.binding;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-10 wenzelm 2008-08-10 pass token source to typ/term etc.;
2008-08-09 wenzelm 2008-08-09 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);
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper;
2008-06-28 wenzelm 2008-06-28 tuned nested args parser; export generic_args1;
2008-06-28 wenzelm 2008-06-28 added thm_name, opt_thm_name;
2008-06-26 wenzelm 2008-06-26 added context/theory scanner;
2008-06-16 wenzelm 2008-06-16 export eof;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2007-11-08 wenzelm 2007-11-08 added const_proper;
2007-11-07 wenzelm 2007-11-07 Syntax.read_typ;
2007-11-07 wenzelm 2007-11-07 removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-13 wenzelm 2007-08-13 Lexicon.read_indexname/nat/variable;
2007-07-27 wenzelm 2007-07-27 added terminator, named_attribute;
2007-05-11 wenzelm 2007-05-11 bang_facts: warning;
2007-04-14 wenzelm 2007-04-14 Morphism.transform/form;
2007-01-02 wenzelm 2007-01-02 Morphism.fact;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-09 wenzelm 2006-12-09 added term_abbrev;
2006-12-07 wenzelm 2006-12-07 tuned pretty_src output;
2006-12-05 wenzelm 2006-12-05 attribute value: morphism;
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;