src/Provers/classical.ML
2007-05-31 ago simplified/unified list fold;
2007-05-07 ago simplified DataFun interfaces;
2007-04-14 ago canonical merge operations
2007-03-20 ago fixed slip
2007-03-19 ago moved Output.overwrite_warn here
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-01-19 ago moved ML context stuff to from Context to ML_Context;
2006-12-30 ago removed obsolete name_hint handling;
2006-12-07 ago Removal of theorem tagging, which the ATP linkup no longer requires,
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-11-24 ago ProofContext.init;
2006-10-11 ago Toplevel: generic_theory;
2006-06-13 ago Drule.equiv_thm supercedes Drule.weak_eq_thm;
2006-03-14 ago ObjectLogic.is_elim;
2006-02-20 ago moved intro_classes from AxClass to ClassPackage
2006-02-10 ago tuned;
2006-01-29 ago default rule step: norm_hhf_tac;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-15 ago attributes: optional weight;
2006-01-14 ago generic attributes;
2006-01-10 ago generic attributes;
2006-01-05 ago store_thm: transfer to current context, i.e. the target theory;
2006-01-04 ago preservation of names
2006-01-03 ago Provers/classical: stricter checks to ensure that supplied intro, dest and
2005-12-31 ago added classical_rule, which replaces Data.make_elim;
2005-12-08 ago swap: no longer pervasive;
2005-11-22 ago Drule.multi_resolves;
2005-10-28 ago Added "deepen" method.
2005-10-17 ago change_claset(_of): more abtract interface;
2005-10-08 ago minor tweaks for Poplog/PML;
2005-09-05 ago introduced binding priority 1 for linear combinators etc.
2005-08-16 ago classical rules must have names for ATP integration
2005-08-16 ago OuterKeyword;
2005-07-13 ago removed obsolete delta stuff;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-04-15 ago Removed most of the atp interface from Pure.
2005-04-13 ago *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-21 ago Jia Meng: delta simpsets and clasets
2004-07-11 ago context dependent components;
2004-04-16 ago 'instance' and intro_classes now handle general sorts;
2002-08-27 ago dup_elim: improved error reporting;
2002-05-07 ago use eq_thm_prop instead of slightly inadequate eq_thm;
2001-12-06 ago added 'swapped' attribute;
2001-12-05 ago simplified (and clarified) integration with Pure/ContextRules;
2001-12-04 ago made SML/NJ happy;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-08 ago theory data: finish method;
2001-11-05 ago Method.trace ctxt;
2001-10-15 ago Tactic.orderlist;
2001-10-14 ago ObjectLogic.atomize_tac;
2001-10-12 ago moved trace_rules to Pure/Isar/method.ML;
2001-02-23 ago renamed addaltern to addafter, addSaltern to addSafter
2001-02-20 ago corrected comments on addbefore and addSbefore
2001-01-07 ago CHANGED_PROP;