2010-09-03 ago turned show_consts into proper configuration option;
2010-09-02 ago turned show_question_marks into proper configuration option;
2010-08-11 ago tuned eval_thms (cf. note etc. in proof.ML);
2010-08-11 ago use Pretty.enum convenience;
2010-05-30 ago replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information;
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-05-10 ago renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 ago pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
2010-03-28 ago configuration options admit dynamic default values;
2010-03-28 ago do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
2010-03-26 ago replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-07 ago modernized structure Object_Logic;
2010-03-07 ago modernized structure Local_Defs;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-30 ago Added "constraints" tag / attribute for specifying the number of equality
2009-11-13 ago eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-08 ago adapted Theory_Data;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-25 ago make SML/NJ happy;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-02 ago merged, resolving conflict in src/Pure/Isar/attrib.ML;
2009-06-02 ago made SML/NJ happy
2009-06-01 ago made SML/NJ happy;
2009-05-30 ago eliminated old Attrib.add_attributes (and Attrib.syntax);
2009-05-30 ago modernized attribute setup;
2009-05-18 ago introduced Thm.generatedK
2009-05-16 ago added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 ago added map_facts_refs;
2009-03-18 ago more precise type Symbol_Pos.text;
2009-03-16 ago tuned signature;
2009-03-15 ago added setup and attribute_setup -- expect plain parser instead of syntax function;
2009-03-13 ago eliminated type Args.T;
2009-03-12 ago renamed NameSpace.bind to NameSpace.define;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago Thm.binding;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-29 ago Added abs_def attribute.
2009-01-21 ago binding is alias for Binding.T
2008-12-05 ago removed Table.extend, NameSpace.extend_table
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-10 ago pass position to get_fact;
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-08-06 ago report markup;
2008-08-04 ago tuned signature;
2008-05-14 ago added defined;
2008-04-17 ago no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
2008-04-16 ago PureThy.get_fact: pass dynamic context;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-20 ago Facts.Named: include position;
2008-03-20 ago renamed former get_thms(_silent) to get_fact(_silent);