10 months ago wenzelm 2019-07-24 avoid global syntax for MinProof (amending e31271559de8);
10 months ago wenzelm 2019-07-21 global declaration of abstract syntax for proof terms, with qualified names; clarified modules;
2018-02-25 wenzelm 2018-02-25 eliminated ASCII syntax from Pure bootstrap; tuned comments;
2018-02-25 wenzelm 2018-02-25 notation for dummy sort;
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-08-04 wenzelm 2016-08-04 prefer hardwired "nothing";
2016-04-01 wenzelm 2016-04-01 explicit property for unbreakable block;
2016-03-30 wenzelm 2016-03-30 clarified simple mixfix;
2016-03-29 wenzelm 2016-03-29 more position information for type mixfix;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2016-01-09 wenzelm 2016-01-09 discontinued \<struct> syntax;
2015-12-29 wenzelm 2015-12-29 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; uniform syntax for Pure.imp; removed obsolete "HTML" syntax;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-09-09 wenzelm 2015-09-09 eliminated \<Colon> from syntax of constraints;
2014-09-22 wenzelm 2014-09-22 discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-20 wenzelm 2014-03-20 produce qualified names more directly;
2014-01-22 wenzelm 2014-01-22 inner syntax token language allows regular quoted strings; tuned signature;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-05-28 wenzelm 2013-05-28 explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;
2013-05-26 wenzelm 2013-05-26 tuned;
2013-05-26 wenzelm 2013-05-26 tuned signature;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-04-04 wenzelm 2013-04-04 added var_position in analogy to longid_position, for typing reports on input; avoid duplicate token var report;
2012-12-30 wenzelm 2012-12-30 uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
2012-12-19 nipkow 2012-12-19 removed odd associativity of ==
2012-10-03 wenzelm 2012-10-03 allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;
2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2012-02-15 wenzelm 2012-02-15 renamed "xstr" to "str_token";
2012-01-16 wenzelm 2012-01-16 position constraints for numerals enable PIDE markup;
2011-12-01 wenzelm 2011-12-01 renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
2011-11-14 wenzelm 2011-11-14 inner syntax positions for string literals;
2011-11-07 wenzelm 2011-11-07 discontinued numbered structure indexes (legacy feature);
2011-08-22 wenzelm 2011-08-22 special treatment of structure index 1 in Pure, including legacy warning;
2011-04-19 wenzelm 2011-04-19 less bulky "_position", for improved readability of parse trees;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-08 wenzelm 2011-04-08 discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 wenzelm 2011-04-08 CONST syntax with positions;
2011-04-08 wenzelm 2011-04-08 moved CONST syntax/translations to their proper place;
2011-04-08 wenzelm 2011-04-08 simplified Pure syntax bootstrap;
2011-04-08 wenzelm 2011-04-08 renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-06 wenzelm 2011-04-06 type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2011-03-22 wenzelm 2011-03-22 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-22 wenzelm 2011-03-22 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_) variants;
2010-09-01 wenzelm 2010-09-01 actually declare "_constrainAbs" as @{syntax_const};