src/Pure/pure_thy.ML
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_)Position.report variants;
2010-09-01 wenzelm 2010-09-01 actually declare "_constrainAbs" as @{syntax_const};
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-04-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 wenzelm 2010-03-21 minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-16 wenzelm 2010-02-16 moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2009-11-15 wenzelm 2009-11-15 eliminated obsolete thm position tags;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Simple_Syntax;
2009-10-30 haftmann 2009-10-30 set Pure theory name properly
2009-10-25 wenzelm 2009-10-25 maintain group via name space, not tags;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-07-21 wenzelm 2009-07-21 join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;
2009-07-19 wenzelm 2009-07-19 cancel_proofs: some attempts at reworking group management (based on body promises only);
2009-04-02 wenzelm 2009-04-02 tuned signature;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-07 wenzelm 2009-03-07 Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-10 wenzelm 2009-01-10 added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10 wenzelm 2009-01-10 tuned;
2009-01-10 wenzelm 2009-01-10 simplified join_proofs;
2008-12-23 wenzelm 2008-12-23 renamed terminal category "float" to "float_token", to avoid name space conflicts with actual "float" types in user theories (only "float_const" is encountered in practice anyway); tuned;