src/Provers/classical.ML
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;
2011-05-14 wenzelm 2011-05-14 method "deepen" with optional limit;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-13 wenzelm 2011-05-13 do not open ML structures;
2011-05-13 wenzelm 2011-05-13 eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);
2011-05-13 wenzelm 2011-05-13 misc tuning and simplification;
2011-04-20 wenzelm 2011-04-20 eliminated Display.string_of_thm_without_context; tuned whitespace;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-15 wenzelm 2011-01-15 clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
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-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
2009-10-02 wenzelm 2009-10-02 eliminated dead code and redundant parameters; tuned;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-29 wenzelm 2009-07-29 removed old global get_claset/map_claset; added local get_claset/put_claset;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-17 wenzelm 2009-03-17 renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2009-03-15 wenzelm 2009-03-15 simplified method setup;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-31 wenzelm 2008-12-31 use exists_subterm directly;
2008-05-17 wenzelm 2008-05-17 tuned comments;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset; tuned signature;
2008-03-28 haftmann 2008-03-28 unfold_locales now part of default tactic
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-26 wenzelm 2008-03-26 pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-08-20 wenzelm 2007-08-20 tuned merge operations via pointer_eq;
2007-08-10 haftmann 2007-08-10 ClassPackage renamed to Class