src/Provers/classical.ML
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;
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-11-20 wenzelm 1997-11-20 adapted print methods;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-11-03 wenzelm 1997-11-03 new implicit claset mechanism based on Sign.sg anytype data; tuned warnings;
1997-11-01 paulson 1997-11-01 Fixed comments
1997-09-29 paulson 1997-09-29 Added Safe_tac; all other default claset tactics now dereference "claset" only when given the proof state
1997-09-25 paulson 1997-09-25 Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
1997-07-22 wenzelm 1997-07-22 improved print_cs;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-05-15 oheimb 1997-05-15 corrected depth_tac: no call for safe_step_tac if subgoal not present
1997-04-02 paulson 1997-04-02 New DEEPEN allows giving an upper bound for deepen_tac
1997-03-19 paulson 1997-03-19 delrules now deletes ALL occurrences of a rule, since it may appear in any of the four lists.
1997-02-28 paulson 1997-02-28 dup_intr & dup_elim no longer call standard -- this lets them be used on meta-hyps
1997-02-15 oheimb 1997-02-15 moved THEN_MAYBE to Pure/tctical.ML better addbefore, addafter (now: addaltern), setwrapper (now: setWrapper) and addwrapper (now addWrapper) added safe wrapper(and functions setSWrapper,compSWrapper,addSbefore,addSaltern)
1996-11-12 paulson 1996-11-12 Added a comment
1996-10-08 paulson 1996-10-08 Introduction of Slow_tac and Slow_best_tac
1996-08-22 paulson 1996-08-22 Now deepen_tac can take advantage of wrappers -- including addss...
1996-08-20 paulson 1996-08-20 New classical reasoner: warns of, and ignores, redundant rules. Also warns of rules supplied with different "hints" (Safe, etc.)
1996-06-18 paulson 1996-06-18 Addition of Safe_step_tac
1996-06-17 paulson 1996-06-17 Now exports Delrules
1996-06-14 paulson 1996-06-14 Now implements delrules
1996-05-07 berghofe 1996-05-07 Added functions for default claset.
1996-05-01 paulson 1996-05-01 Provides merge_cs to support default clasets
1996-03-15 paulson 1996-03-15 Now provides astar versions (thanks to Norbert Voelker)
1996-02-28 paulson 1996-02-28 imp_elim and swap are now stored in thm database
1995-08-18 paulson 1995-08-18 clarified comment
1995-04-28 lcp 1995-04-28 Recoded addSIs, etc., so that nets are built incrementally instead of from scratch each time. The old approach used excessive time (>1 sec for adding a rule to ZF_cs) and probably excessive space. Now rep_claset includes all record fields. joinrules no longer sorts the rules on number of subgoals, since it does not see the full set of them; instead the number of subgoals modifies the priority.
1995-04-06 lcp 1995-04-06 Added comment.
1995-03-30 lcp 1995-03-30 Addition of wrappers for integration with the simplifier. New infixes setwrapper compwrapper addbefore addafter. New function getwrapper. The wrapper is a tactical that is applied to the step tactic. By default it is the identity. Using THEN one can cause other tactics to be tried before or after the step tactic. Other effects are possible using ORELSE, etc.
1994-11-25 lcp 1994-11-25 deepen_tac: modified due to outcome of experiments. Its choice of unsafe rule to expand is still non-deterministic.
1994-11-02 lcp 1994-11-02 Provers/classical: now takes theorem "classical" as argument, proves "swap" Provers/classical/depth_tac,deepen_tac: new
1994-07-12 lcp 1994-07-12 chain_tac: deleted; just use etac mp
1993-10-15 lcp 1993-10-15 classical/swap_res_tac: recoded to allow backtracking
1993-09-16 clasohm 1993-09-16 Initial revision