src/Provers/classical.ML
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;
2006-12-07 paulson 2006-12-07 Removal of theorem tagging, which the ATP linkup no longer requires,
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-10-11 wenzelm 2006-10-11 Toplevel: generic_theory;
2006-06-13 wenzelm 2006-06-13 Drule.equiv_thm supercedes Drule.weak_eq_thm;
2006-03-14 wenzelm 2006-03-14 ObjectLogic.is_elim;
2006-02-20 haftmann 2006-02-20 moved intro_classes from AxClass to ClassPackage
2006-02-10 wenzelm 2006-02-10 tuned;
2006-01-29 wenzelm 2006-01-29 default rule step: norm_hhf_tac;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-15 wenzelm 2006-01-15 attributes: optional weight; tuned;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2006-01-10 wenzelm 2006-01-10 generic attributes;
2006-01-05 wenzelm 2006-01-05 store_thm: transfer to current context, i.e. the target theory;
2006-01-04 paulson 2006-01-04 preservation of names
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2005-12-31 wenzelm 2005-12-31 added classical_rule, which replaces Data.make_elim; removed obsolete Data.make_elim and classical elim_format attribute; tuned;
2005-12-08 wenzelm 2005-12-08 swap: no longer pervasive;
2005-11-22 wenzelm 2005-11-22 Drule.multi_resolves;
2005-10-28 berghofe 2005-10-28 Added "deepen" method.
2005-10-17 wenzelm 2005-10-17 change_claset(_of): more abtract interface; claset_of: init proof context; added raw get_claset;
2005-10-08 wenzelm 2005-10-08 minor tweaks for Poplog/PML;
2005-09-05 haftmann 2005-09-05 introduced binding priority 1 for linear combinators etc.
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-07-13 wenzelm 2005-07-13 removed obsolete delta stuff;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun;
2005-04-15 ballarin 2005-04-15 Removed most of the atp interface from Pure.
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Method.src;