src/Provers/classical.ML
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;
2000-12-23 ago recover_order for single step tules;
2000-11-04 ago tuned method "rule" and "default";
2000-11-03 ago atomize: all automated tactics that "solve" goals;
2000-10-23 ago intro_classes by default;
2000-10-11 ago fixed 'clarify': CHANGED;
2000-09-19 ago tuned args;
2000-09-13 ago Args.addN, Args.delN;
2000-09-12 ago renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12 ago delrule: handle dest rules as well;
2000-09-07 ago tuned att names / msgs;
2000-09-02 ago added "slow";
2000-09-01 ago added "safe" method;
2000-08-31 ago improved messages;
2000-08-29 ago *** empty log message ***
2000-08-09 ago fixed classification of rules in atts and modifiers (final!?);
2000-08-03 ago unknown_theory/proof/context;
2000-07-27 ago intro_elim_tac: bimatch_from;
2000-07-25 ago added clarify method;
2000-07-23 ago classical atts now intro! / intro / intro?;
2000-07-21 ago strengthened force_tac by using new first_best_tac
2000-06-28 ago classical 'elimify' attribute;
2000-06-28 ago uses a supplied version of make_elim for addDs
2000-05-31 ago Toplevel.no_timing;
2000-05-23 ago improved warning messages;
2000-04-17 ago Pretty.chunks;
2000-04-13 ago intro/elim_tac: match only;