--- 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);