2010-05-17 ago renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-03-13 ago removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-06 ago eliminated Args.bang_facts (legacy feature);
2010-02-27 ago clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-25 ago clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-06 ago fixed spelling;
2009-11-10 ago bang_facts: legacy feature;
2009-09-30 ago eliminated redundant bindings;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-18 ago de-camelized Symbol_Pos;
2009-03-13 ago simplified goal_spec: default to first goal;
2009-03-13 ago eliminated type Args.T;
2009-03-12 ago Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-03 ago 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;
2009-01-21 ago removed Ids;
2009-01-21 ago binding is alias for Binding.T
2008-12-04 ago cleaned up binding module and related code
2008-12-01 ago new Binding module
2008-09-02 ago added binding;
2008-08-15 ago Args.name_source(_position) for proper position information;
2008-08-10 ago pass token source to typ/term etc.;
2008-08-09 ago unified Args.T with OuterLex.token;
2008-08-04 ago abstract type Scan.stopper;
2008-06-28 ago tuned nested args parser;
2008-06-28 ago added thm_name, opt_thm_name;
2008-06-26 ago added context/theory scanner;
2008-06-16 ago export eof;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-28 ago added ::: / @@@ scanner combinators;
2007-11-08 ago added const_proper;
2007-11-07 ago Syntax.read_typ;
2007-11-07 ago removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-09-01 ago replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-13 ago Lexicon.read_indexname/nat/variable;
2007-07-27 ago added terminator, named_attribute;
2007-05-11 ago bang_facts: warning;
2007-04-14 ago Morphism.transform/form;
2007-01-02 ago Morphism.fact;
2006-12-18 ago switched argument order in *.syntax lifters
2006-12-09 ago added term_abbrev;
2006-12-07 ago tuned pretty_src output;
2006-12-05 ago attribute value: morphism;
2006-11-23 ago renamed Name value to Text, which is *not* a name in terms of morphisms;
2006-11-23 ago replaced map_values by morph_values;
2006-10-14 ago moved pretty_attribs to attrib.ML;
2006-09-21 ago member (op =);
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-30 ago added maxidx_values;
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-12 ago query/bang_colon: separate tokens;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-02-10 ago Context.generic is canonical state of parsers;
2006-01-21 ago simplified type attribute;
2006-01-10 ago added generic syntax;
2005-10-28 ago syntax for literal facts;
2005-08-18 ago removed obsolete Theory.sign_of;
2005-08-16 ago added liberal_name;