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