src/Provers/classical.ML
2002-08-27 wenzelm 2002-08-27 dup_elim: improved error reporting;
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2001-12-06 wenzelm 2001-12-06 added 'swapped' attribute; tuned xtra_netpair; tuned;
2001-12-05 wenzelm 2001-12-05 simplified (and clarified) integration with Pure/ContextRules; removed "extra" rules as separate slots, only keep xtra_netpair for single-step view of plain haz/safe rules;
2001-12-04 wenzelm 2001-12-04 made SML/NJ happy;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2001-11-05 wenzelm 2001-11-05 Method.trace ctxt;
2001-10-15 wenzelm 2001-10-15 Tactic.orderlist;
2001-10-14 wenzelm 2001-10-14 ObjectLogic.atomize_tac;
2001-10-12 wenzelm 2001-10-12 moved trace_rules to Pure/Isar/method.ML; some_rule_tac: prefer Method.some_rule_tac of Pure, no special handling of imp_elim;
2001-02-23 oheimb 2001-02-23 renamed addaltern to addafter, addSaltern to addSafter
2001-02-20 oheimb 2001-02-20 corrected comments on addbefore and addSbefore
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2000-12-23 wenzelm 2000-12-23 recover_order for single step tules;
2000-11-04 wenzelm 2000-11-04 tuned method "rule" and "default";
2000-11-03 wenzelm 2000-11-03 atomize: all automated tactics that "solve" goals;
2000-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-10-11 wenzelm 2000-10-11 fixed 'clarify': CHANGED;
2000-09-19 wenzelm 2000-09-19 tuned args;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12 wenzelm 2000-09-12 delrule: handle dest rules as well; replaced "delrule" by "rule del";
2000-09-07 wenzelm 2000-09-07 tuned att names / msgs;
2000-09-02 wenzelm 2000-09-02 added "slow";
2000-09-01 wenzelm 2000-09-01 added "safe" method;
2000-08-31 wenzelm 2000-08-31 improved messages;
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-09 wenzelm 2000-08-09 fixed classification of rules in atts and modifiers (final!?);
2000-08-03 wenzelm 2000-08-03 unknown_theory/proof/context;
2000-07-27 wenzelm 2000-07-27 intro_elim_tac: bimatch_from;
2000-07-25 wenzelm 2000-07-25 added clarify method; removed unofficial improper methods;
2000-07-23 wenzelm 2000-07-23 classical atts now intro! / intro / intro?;
2000-07-21 oheimb 2000-07-21 strengthened force_tac by using new first_best_tac
2000-06-28 wenzelm 2000-06-28 classical 'elimify' attribute;
2000-06-28 paulson 2000-06-28 uses a supplied version of make_elim for addDs
2000-05-31 wenzelm 2000-05-31 Toplevel.no_timing;
2000-05-23 wenzelm 2000-05-23 improved warning messages;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-04-13 wenzelm 2000-04-13 intro/elim_tac: match only;
2000-04-05 wenzelm 2000-04-05 HEADGOAL;
2000-04-04 wenzelm 2000-04-04 print_simpset / print_claset command;
2000-03-18 wenzelm 2000-03-18 tuned comments;
2000-03-15 wenzelm 2000-03-15 tuned comments;
2000-03-08 wenzelm 2000-03-08 fixed section syntax;
2000-03-04 wenzelm 2000-03-04 REPEAT_ALL_NEW;
2000-02-07 wenzelm 2000-02-07 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
2000-01-28 wenzelm 2000-01-28 HEADGOAL;
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!);
2000-01-05 wenzelm 2000-01-05 METHOD_CLASET': refer to *local* claset;
1999-09-21 wenzelm 1999-09-21 setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts;
1999-09-01 wenzelm 1999-09-01 Method.insert_tac; Method.multi_resolves; contradiction: made faithful; tuned comments;
1999-08-25 wenzelm 1999-08-25 proper setup of GlobalClaset data;
1999-08-24 wenzelm 1999-08-24 fixed intro_elim_tac;
1999-08-20 wenzelm 1999-08-20 intro/elim: REPEAT1;
1999-08-19 wenzelm 1999-08-19 renamed 'some_rule' to 'rule';
1999-08-18 wenzelm 1999-08-18 Method.modifier;
1999-08-17 wenzelm 1999-08-17 renamed 'single' to 'some_rule'; added 'intro', 'elim';
1999-08-02 wenzelm 1999-08-02 export cla_meth(');
1999-07-30 wenzelm 1999-07-30 eliminated METHOD0 in favour of same_tac;