src/Pure/Isar/args.ML
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-03-13 wenzelm 2010-03-13 removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-02-27 wenzelm 2010-02-27 clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-06 wenzelm 2010-02-06 fixed spelling;
2009-11-10 wenzelm 2009-11-10 bang_facts: legacy feature;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-13 wenzelm 2009-03-13 simplified goal_spec: default to first goal;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-03 wenzelm 2009-03-03 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
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;