src/Pure/Isar/method.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-08-16 wenzelm 2013-08-16 more markup via Name_Space.check; tuned signature;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-03-09 wenzelm 2013-03-09 tuned;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-10-17 wenzelm 2012-10-17 more method position information, notably finished_pos after end of previous text;
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-13 wenzelm 2012-10-13 refined Proof.the_finished_goal with more informative error; more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure; clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-03-03 wenzelm 2012-03-03 canonical argument order for attribute application;
2012-02-14 wenzelm 2012-02-14 tuned signature, according to actual usage of these operations;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-10-21 wenzelm 2011-10-21 tuned;
2011-05-15 wenzelm 2011-05-15 optional description for 'attribute_setup' and 'method_setup';
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-17 wenzelm 2011-04-17 markup attributes/methods via name space; eliminated obsolete markup;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-12-21 wenzelm 2010-12-21 configuration option "rule_trace"; discontinued preference "trace-rules";
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-07 ballarin 2010-04-07 Merged resolving conflicts NEWS and locale.ML.
2010-02-15 ballarin 2010-02-15 Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-17 wenzelm 2009-10-17 Method.cheating: check quick_and_dirty here;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-25 wenzelm 2009-07-25 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-05-30 wenzelm 2009-05-30 eliminated old Method.add_method(s);
2009-05-30 wenzelm 2009-05-30 removed obsolete combinators for method args;
2009-05-23 wenzelm 2009-05-23 removed some obsolete combinators for method args;
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text;
2009-03-17 wenzelm 2009-03-17 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 wenzelm 2009-03-16 adapted 'method_setup' command to Method.setup;
2009-03-15 wenzelm 2009-03-15 export section, sections; tuned signature;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 added simplified setup; eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-04 blanchet 2009-03-04 Merge.