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

author | nipkow |

Fri, 17 Jan 2003 15:39:29 +0100 | |

changeset 13781 | ecb2df44253e |

parent 13780 | af7b79271364 |

child 13782 | 44de406a7273 |

*** empty log message ***

--- a/NEWS Wed Jan 15 16:45:32 2003 +0100 +++ b/NEWS Fri Jan 17 15:39:29 2003 +0100 @@ -6,45 +6,40 @@ *** General *** -* Provers/linorder: New generic prover for transitivity reasoning over -linear orders. Note: this prover is not efficient! - * Provers/simplifier: - - Completely reimplemented Asm_full_simp_tac: + - Completely reimplemented method simp (ML: Asm_full_simp_tac): Assumptions are now subject to complete mutual simplification, not just from left to right. The simplifier now preserves the order of assumptions. Potential INCOMPATIBILITY: - -- Asm_full_simp_tac sometimes diverges where the old version did - not, e.g. invoking Asm_full_simp_tac on the goal + -- simp sometimes diverges where the old version did + not, e.g. invoking simp on the goal [| P (f x); y = x; f x = f y |] ==> Q - now gives rise to the infinite reduction sequence - - P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ... - - Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead - often solves this kind of problem. - - -- Tactics combining classical reasoner and simplification (such - as auto) are also affected by this change, because many of them - rely on Asm_full_simp_tac. They may sometimes diverge as well - or yield a different numbers of subgoals. Try to use e.g. force, - fastsimp, or safe instead of auto in case of problems. Sometimes - subsequent calls to the classical reasoner will fail because a - preceeding call to the simplifier too eagerly simplified the - goal, e.g. deleted redundant premises. + now gives rise to the infinite reduction sequence + + P(f x) --(f x = f y)--> P(f y) --(y = x)--> P(f x) --(f x = f y)--> ... + + Using "simp (asm_lr)" (ML: Asm_lr_simp_tac) instead often solves this + kind of problem. + + -- Tactics combining classical reasoner and simplification (such as auto) + are also affected by this change, because many of them rely on + simp. They may sometimes diverge as well or yield a different numbers + of subgoals. Try to use e.g. force, fastsimp, or safe instead of auto + in case of problems. Sometimes subsequent calls to the classical + reasoner will fail because a preceeding call to the simplifier too + eagerly simplified the goal, e.g. deleted redundant premises. - The simplifier trace now shows the names of the applied rewrite rules -* Pure: new flag trace_unify_fail causes unification to print -diagnostic information (PG: in trace buffer) when it fails. This is -useful for figuring out why single step proofs like rule, erule or -assumption failed. +* Pure: new flag for triggering if the overall goal of a proof state should +be printed (ML: Proof.show_main_goal). +PG menu: Isabelle/Isar -> Settigs -> Show Main Goal * Pure: you can find all matching introduction rules for subgoal 1, i.e. all rules whose conclusion matches subgoal 1, by executing @@ -54,6 +49,11 @@ (or rather last, the way it is printed). TODO: integration with PG +* Pure: new flag trace_unify_fail causes unification to print +diagnostic information (PG: in trace buffer) when it fails. This is +useful for figuring out why single step proofs like rule, erule or +assumption failed. + * Pure: locale specifications now produce predicate definitions according to the body of text (covering assumptions modulo local definitions); predicate "loc_axioms" covers newly introduced text, @@ -84,6 +84,9 @@ are regarded as potentially overloaded, which improves robustness in exchange for slight decrease in efficiency; +* Provers/linorder: New generic prover for transitivity reasoning over +linear orders. Note: this prover is not efficient! + * Isar: preview of problems to finish 'show' now produce an error rather than just a warning (in interactive mode);