63 |
63 |
64 * minor changes in semantics of addafter (now called addaltern); renamed |
64 * minor changes in semantics of addafter (now called addaltern); renamed |
65 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper |
65 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper |
66 (and access functions for it); |
66 (and access functions for it); |
67 |
67 |
68 * improved combination of classical reasoner and simplifier: new |
68 * improved combination of classical reasoner and simplifier: |
69 addss, auto_tac, functions for handling clasimpsets, ... Now, the |
69 + functions for handling clasimpsets |
70 simplification is safe (therefore moved to safe_step_tac) and thus |
70 + improvement of addss: now the simplifier is called _after_ the |
71 more complete, as multiple instantiation of unknowns (with slow_tac). |
71 safe steps. |
72 COULD MAKE EXISTING PROOFS FAIL; in case of problems with |
72 + safe variant of addss called addSss: uses safe simplifications |
73 old proofs, use unsafe_addss and unsafe_auto_tac; |
73 _during_ the safe steps. It is more complete as it allows multiple |
74 |
74 instantiations of unknowns (e.g. with slow_tac). |
75 |
75 |
76 *** Simplifier *** |
76 *** Simplifier *** |
77 |
77 |
78 * added interface for simplification procedures (functions that |
78 * added interface for simplification procedures (functions that |
79 produce *proven* rewrite rules on the fly, depending on current |
79 produce *proven* rewrite rules on the fly, depending on current |