src/Provers/classical.ML
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