src/Provers/classical.ML
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-09 wenzelm 2016-04-09 removed old proof method "default";
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-10-05 wenzelm 2015-10-05 tuned signature;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-08-30 wenzelm 2015-08-30 store result of swapify, to avoid later access to implicit context;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-08-16 wenzelm 2015-08-16 delete precisely the added rules; tuned;
2015-08-16 wenzelm 2015-08-16 clarified context;
2015-08-16 wenzelm 2015-08-16 tuned whitespace;
2015-08-16 wenzelm 2015-08-16 tuned signature;
2015-08-16 wenzelm 2015-08-16 tuned;
2015-07-28 wenzelm 2015-07-28 clarified context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-05 wenzelm 2015-07-05 clarified context;
2015-06-30 wenzelm 2015-06-30 no arguments for "standard" (or old "default") methods;
2015-06-30 wenzelm 2015-06-30 renamed "default" to "standard", to make semantically clear what it is;
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-12-20 wenzelm 2014-12-20 proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
2014-12-09 wenzelm 2014-12-09 tuned spelling;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context;
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-05 wenzelm 2014-08-05 more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
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-07-27 wenzelm 2013-07-27 standardized aliases;
2013-07-18 wenzelm 2013-07-18 tuned signature;
2013-06-27 wenzelm 2013-06-27 actually use Data.sizef, not hardwired size_of_thm;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 tuned signature;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 wenzelm 2013-04-12 modifiers for classical wrappers operate on Proof.context instead of claset;
2013-04-10 wenzelm 2013-04-10 obsolete -- tools should refer to proper Proof.context;
2013-04-09 wenzelm 2013-04-09 discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-29 wenzelm 2013-03-29 Pretty.item markup for improved readability of lists of items;
2012-11-17 wenzelm 2012-11-17 tuned -- eliminate pointless ML method definition;
2012-11-17 wenzelm 2012-11-17 method setup for Classical steps;
2012-11-03 wenzelm 2012-11-03 more concise/precise documentation;
2012-06-25 wenzelm 2012-06-25 prefer direct rotate_prems over old-style COMP;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-12 wenzelm 2012-03-12 tuned signature;
2012-02-14 wenzelm 2012-02-14 eliminated obsolete aliases;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-05-15 wenzelm 2011-05-15 tuned;
2011-05-15 wenzelm 2011-05-15 tuned signature;
2011-05-14 wenzelm 2011-05-14 slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
2011-05-14 wenzelm 2011-05-14 more precise warnings: observe context visibility;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;