2011-04-17 ago markup attributes/methods via name space;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-12-21 ago configuration option "rule_trace";
2010-09-17 ago tuned signature of (Context_) variants;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
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-04-07 ago Merged resolving conflicts NEWS and locale.ML.
2010-02-15 ago Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-03-07 ago modernized structure Object_Logic;
2010-03-07 ago modernized structure Local_Defs;
2009-11-08 ago adapted Theory_Data;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-01 ago modernized structure Context_Rules;
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-10-17 ago Method.cheating: check quick_and_dirty here;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-25 ago basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
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-05-30 ago eliminated old Method.add_method(s);
2009-05-30 ago removed obsolete combinators for method args;
2009-05-23 ago removed some obsolete combinators for method args;
2009-03-18 ago more precise type Symbol_Pos.text;
2009-03-17 ago close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
2009-03-16 ago adapted 'method_setup' command to Method.setup;
2009-03-15 ago export section, sections;
2009-03-13 ago simplified method setup;
2009-03-13 ago added simplified setup;
2009-03-13 ago tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
2009-03-12 ago renamed NameSpace.bind to NameSpace.define;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-04 ago renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-01 ago use long names for old-style fold combinators;
2009-02-28 ago moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-11 ago FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-01-01 ago assumption/close: discontinued implicit prems;
2008-12-05 ago removed Table.extend, NameSpace.extend_table
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-06-28 ago replaced simple_text by fully-featured parse_args;
2008-06-16 ago renamed rename_params_tac to rename_tac;
2008-06-16 ago ML tactic: do not abstract over context again;
2008-05-14 ago added intern, defined;
2008-04-29 ago added lemma antiquotation
2008-03-28 ago ml_tactic: non-critical version via proof data and thread data;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-28 ago reorganized signature of ML_Context;
2008-03-27 ago eliminated delayed theory setup
2008-03-26 ago adapted to Context.thread_data interface;
2008-03-24 ago ML runtime compilation: pass position, tuned signature;
2008-03-15 ago tuned messages;