src/Provers/classical.ML
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;
2000-04-05 ago HEADGOAL;
2000-04-04 ago print_simpset / print_claset command;
2000-03-18 ago tuned comments;
2000-03-15 ago tuned comments;
2000-03-08 ago fixed section syntax;
2000-03-04 ago REPEAT_ALL_NEW;
2000-02-07 ago intro/elim/dest attributes: changed ! / !! flags to ? / ??;
2000-01-28 ago HEADGOAL;
2000-01-28 ago replaced FIRSTGOAL by FINDGOAL (backtracking!);
2000-01-05 ago METHOD_CLASET': refer to *local* claset;
1999-09-21 ago setup for refined facts handling;
1999-09-01 ago Method.insert_tac;
1999-08-25 ago proper setup of GlobalClaset data;
1999-08-24 ago fixed intro_elim_tac;
1999-08-20 ago intro/elim: REPEAT1;
1999-08-19 ago renamed 'some_rule' to 'rule';
1999-08-18 ago Method.modifier;
1999-08-17 ago renamed 'single' to 'some_rule';
1999-08-02 ago export cla_meth(');
1999-07-30 ago eliminated METHOD0 in favour of same_tac;
1999-07-27 ago safe_step_tac / step_tac;
1999-07-14 ago tuned contradiction method;
1999-07-10 ago dup_elim: use try to handle general exn;
1999-07-09 ago type claset: added extra I/E rules;
1999-04-30 ago theory data: copy;
1999-04-23 ago improved 'single' method;
1999-04-23 ago oops;
1999-04-22 ago single method: include not_elim, imp_elim;
1999-04-14 ago cleaned comments;
1999-03-17 ago Theory.sign_of;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-18 ago expoer cla_method('), cla_modifiers;
1998-11-16 ago tuned attribute names;
1998-11-09 ago local claset theory data;
1998-10-23 ago corrected (and simplified) depth_tac
1998-09-21 ago added addD2, addE2, addSD2, and addSE2
1998-06-10 ago Context.the_context;
1998-06-05 ago accomodate tuned version of theory data;
1998-04-29 ago tuned setup;
1998-04-04 ago type_error;