src/Provers/classical.ML
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
2007-07-28 wenzelm 2007-07-28 added get_cs/map_cs;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; added flat_rule filter for addXXs etc.;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-14 haftmann 2007-04-14 canonical merge operations
2007-03-20 haftmann 2007-03-20 fixed slip
2007-03-19 haftmann 2007-03-19 moved Output.overwrite_warn here
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2006-12-30 wenzelm 2006-12-30 removed obsolete name_hint handling;