summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 21 Oct 1998 13:01:17 +0200 | |

changeset 5705 | 56f2030c46c6 |

parent 5704 | 1ddf7e1e8b19 |

child 5706 | 21706a735c8d |

tuned (all proofs are INSTABLE by David's definition of instability);

--- a/NEWS Wed Oct 21 11:10:38 1998 +0200 +++ b/NEWS Wed Oct 21 13:01:17 1998 +0200 @@ -53,10 +53,11 @@ delWrapper, delSWrapper: claset * string -> claset getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; -* Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE semantics; - addbefore now affects only the unsafe part of step_tac etc.; - This affects addss/auto_tac/force_tac,so EXISTING (INSTABLE) PROOFS MAY FAIL, - but proofs should be fixable easily, e.g. by replacing Auto_tac by Force_tac. +* Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE + semantics; addbefore now affects only the unsafe part of step_tac + etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY + FAIL, but proofs should be fixable easily, e.g. by replacing + Auto_tac by Force_tac; * Classical reasoner: setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper (and access functions for it);