summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 13781 | ecb2df44253e |

parent 13745 | a31e04831dd1 |

child 13815 | 0832792725db |

1.1 --- a/NEWS Wed Jan 15 16:45:32 2003 +0100 1.2 +++ b/NEWS Fri Jan 17 15:39:29 2003 +0100 1.3 @@ -6,45 +6,40 @@ 1.4 1.5 *** General *** 1.6 1.7 -* Provers/linorder: New generic prover for transitivity reasoning over 1.8 -linear orders. Note: this prover is not efficient! 1.9 - 1.10 * Provers/simplifier: 1.11 1.12 - - Completely reimplemented Asm_full_simp_tac: 1.13 + - Completely reimplemented method simp (ML: Asm_full_simp_tac): 1.14 Assumptions are now subject to complete mutual simplification, 1.15 not just from left to right. The simplifier now preserves 1.16 the order of assumptions. 1.17 1.18 Potential INCOMPATIBILITY: 1.19 1.20 - -- Asm_full_simp_tac sometimes diverges where the old version did 1.21 - not, e.g. invoking Asm_full_simp_tac on the goal 1.22 + -- simp sometimes diverges where the old version did 1.23 + not, e.g. invoking simp on the goal 1.24 1.25 [| P (f x); y = x; f x = f y |] ==> Q 1.26 1.27 - now gives rise to the infinite reduction sequence 1.28 - 1.29 - P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ... 1.30 - 1.31 - Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead 1.32 - often solves this kind of problem. 1.33 - 1.34 - -- Tactics combining classical reasoner and simplification (such 1.35 - as auto) are also affected by this change, because many of them 1.36 - rely on Asm_full_simp_tac. They may sometimes diverge as well 1.37 - or yield a different numbers of subgoals. Try to use e.g. force, 1.38 - fastsimp, or safe instead of auto in case of problems. Sometimes 1.39 - subsequent calls to the classical reasoner will fail because a 1.40 - preceeding call to the simplifier too eagerly simplified the 1.41 - goal, e.g. deleted redundant premises. 1.42 + now gives rise to the infinite reduction sequence 1.43 + 1.44 + P(f x) --(f x = f y)--> P(f y) --(y = x)--> P(f x) --(f x = f y)--> ... 1.45 + 1.46 + Using "simp (asm_lr)" (ML: Asm_lr_simp_tac) instead often solves this 1.47 + kind of problem. 1.48 + 1.49 + -- Tactics combining classical reasoner and simplification (such as auto) 1.50 + are also affected by this change, because many of them rely on 1.51 + simp. They may sometimes diverge as well or yield a different numbers 1.52 + of subgoals. Try to use e.g. force, fastsimp, or safe instead of auto 1.53 + in case of problems. Sometimes subsequent calls to the classical 1.54 + reasoner will fail because a preceeding call to the simplifier too 1.55 + eagerly simplified the goal, e.g. deleted redundant premises. 1.56 1.57 - The simplifier trace now shows the names of the applied rewrite rules 1.58 1.59 -* Pure: new flag trace_unify_fail causes unification to print 1.60 -diagnostic information (PG: in trace buffer) when it fails. This is 1.61 -useful for figuring out why single step proofs like rule, erule or 1.62 -assumption failed. 1.63 +* Pure: new flag for triggering if the overall goal of a proof state should 1.64 +be printed (ML: Proof.show_main_goal). 1.65 +PG menu: Isabelle/Isar -> Settigs -> Show Main Goal 1.66 1.67 * Pure: you can find all matching introduction rules for subgoal 1, 1.68 i.e. all rules whose conclusion matches subgoal 1, by executing 1.69 @@ -54,6 +49,11 @@ 1.70 (or rather last, the way it is printed). 1.71 TODO: integration with PG 1.72 1.73 +* Pure: new flag trace_unify_fail causes unification to print 1.74 +diagnostic information (PG: in trace buffer) when it fails. This is 1.75 +useful for figuring out why single step proofs like rule, erule or 1.76 +assumption failed. 1.77 + 1.78 * Pure: locale specifications now produce predicate definitions 1.79 according to the body of text (covering assumptions modulo local 1.80 definitions); predicate "loc_axioms" covers newly introduced text, 1.81 @@ -84,6 +84,9 @@ 1.82 are regarded as potentially overloaded, which improves robustness in exchange 1.83 for slight decrease in efficiency; 1.84 1.85 +* Provers/linorder: New generic prover for transitivity reasoning over 1.86 +linear orders. Note: this prover is not efficient! 1.87 + 1.88 * Isar: preview of problems to finish 'show' now produce an error 1.89 rather than just a warning (in interactive mode); 1.90