src/Provers/classical.ML
2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2013-12-14 ago proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
2013-07-27 ago standardized aliases;
2013-07-18 ago tuned signature;
2013-06-27 ago actually use Data.sizef, not hardwired size_of_thm;
2013-04-27 ago uniform Proof.context for hyp_subst_tac;
2013-04-18 ago tuned signature;
2013-04-18 ago simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 ago modifiers for classical wrappers operate on Proof.context instead of claset;
2013-04-10 ago obsolete -- tools should refer to proper Proof.context;
2013-04-09 ago discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-03-30 ago more item markup;
2013-03-29 ago Pretty.item markup for improved readability of lists of items;
2012-11-17 ago tuned -- eliminate pointless ML method definition;
2012-11-17 ago method setup for Classical steps;
2012-11-03 ago more concise/precise documentation;
2012-06-25 ago prefer direct rotate_prems over old-style COMP;
2012-03-16 ago outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-12 ago tuned signature;
2012-02-14 ago eliminated obsolete aliases;
2011-11-06 ago more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
2011-05-15 ago tuned;
2011-05-15 ago tuned signature;
2011-05-14 ago slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
2011-05-14 ago more precise warnings: observe context visibility;
2011-05-14 ago modernized functor names;
2011-05-14 ago method "deepen" with optional limit;
2011-05-13 ago proper Proof.context for classical tactics;
2011-05-13 ago do not open ML structures;
2011-05-13 ago eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
2011-05-13 ago misc tuning and simplification;
2011-04-20 ago eliminated Display.string_of_thm_without_context;
2011-04-16 ago modernized structure Proof_Context;
2011-01-15 ago clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 ago proper context for rule_by_tactic;
2010-03-07 ago modernized structure Object_Logic;
2010-03-06 ago eliminated Args.bang_facts (legacy feature);
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-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-15 ago replaced String.concat by implode;
2009-10-02 ago eliminated dead code;
2009-10-02 ago eliminated dead code and redundant parameters;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-29 ago removed old global get_claset/map_claset;
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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-07-06 ago structure Thm: less pervasive names;
2009-03-20 ago Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-17 ago renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2009-03-15 ago simplified method setup;
2009-03-15 ago simplified attribute setup;
2009-03-13 ago eliminated type Args.T;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-01 ago use long names for old-style fold combinators;