src/Provers/classical.ML
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;
1999-07-27 wenzelm 1999-07-27 safe_step_tac / step_tac;
1999-07-14 wenzelm 1999-07-14 tuned contradiction method; improved comments;
1999-07-10 wenzelm 1999-07-10 dup_elim: use try to handle general exn;
1999-07-09 wenzelm 1999-07-09 type claset: added extra I/E rules;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-04-23 wenzelm 1999-04-23 improved 'single' method; added 'contradiction' method;
1999-04-23 wenzelm 1999-04-23 oops;
1999-04-22 wenzelm 1999-04-22 single method: include not_elim, imp_elim;
1999-04-14 wenzelm 1999-04-14 cleaned comments;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-18 wenzelm 1998-11-18 expoer cla_method('), cla_modifiers;
1998-11-16 wenzelm 1998-11-16 tuned attribute names; all modifiers turned into attributes; realistic method syntax;
1998-11-09 wenzelm 1998-11-09 local claset theory data; intro, elim, dest, del attributes; single_tac and method; fast, best etc. methods;
1998-10-23 oheimb 1998-10-23 corrected (and simplified) depth_tac
1998-09-21 oheimb 1998-09-21 added addD2, addE2, addSD2, and addSE2 improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-06-10 wenzelm 1998-06-10 Context.the_context;
1998-06-05 wenzelm 1998-06-05 accomodate tuned version of theory data;
1998-04-29 wenzelm 1998-04-29 tuned setup;
1998-04-04 wenzelm 1998-04-04 type_error;
1998-04-04 wenzelm 1998-04-04 replaced thy_data by setup;
1998-04-03 wenzelm 1998-04-03 tuned names;
1998-04-02 oheimb 1998-04-02 introduced functions for updating the wrapper lists merge_cs now uses merge_alists to merge wrapper lists, left cs has precedence!
1998-03-30 oheimb 1998-03-30 merge_cs now also merges safe and unsafe wrappers
1998-03-12 oheimb 1998-03-12 improved coding of delWrapper and delSWrapper
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-02-23 paulson 1998-02-23 Catches bad elim rules, handling exception OPTION
1998-02-12 wenzelm 1998-02-12 oops;
1998-02-12 wenzelm 1998-02-12 tuned print_cs;
1997-12-12 paulson 1997-12-12 More deterministic (?) contr_tac
1997-12-07 wenzelm 1997-12-07 added print_claset;