NEWS
changeset 13618 12290bdce807
parent 13613 531f1f524848
child 13643 c82298745c20
     1.1 --- a/NEWS	Tue Oct 01 14:45:28 2002 +0200
     1.2 +++ b/NEWS	Tue Oct 01 15:03:28 2002 +0200
     1.3 @@ -6,6 +6,38 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Provers/simplifier:
     1.8 +
     1.9 +  - Completely reimplemented Asm_full_simp_tac:
    1.10 +    Assumptions are now subject to complete mutual simplification,
    1.11 +    not just from left to right. The simplifier now preserves
    1.12 +    the order of assumptions.
    1.13 +
    1.14 +    Potential INCOMPATIBILITY:
    1.15 +
    1.16 +    -- Asm_full_simp_tac sometimes diverges where the old version did
    1.17 +       not, e.g. invoking Asm_full_simp_tac on the goal
    1.18 +
    1.19 +        [| P (f x); y = x; f x = f y |] ==> Q
    1.20 +
    1.21 +      now gives rise to the infinite reduction sequence
    1.22 +
    1.23 +        P (f x) --(f x = f y)--> P (f y) --(y = x)--> P (f x) --(f x = f y)--> ...
    1.24 +
    1.25 +      Using Asm_lr_simp_tac (or "simp (asm_lr)" in Isabelle/Isar) instead
    1.26 +      often solves this kind of problem.
    1.27 +
    1.28 +    -- Tactics combining classical reasoner and simplification (such
    1.29 +       as auto) are also affected by this change, because many of them
    1.30 +       rely on Asm_full_simp_tac. They may sometimes diverge as well
    1.31 +       or yield a different numbers of subgoals. Try to use e.g. force,
    1.32 +       fastsimp, or safe instead of auto in case of problems. Sometimes
    1.33 +       subsequent calls to the classical reasoner will fail because a
    1.34 +       preceeding call to the simplifier too eagerly simplified the
    1.35 +       goal, e.g. deleted redundant premises.
    1.36 +
    1.37 +  - The simplifier trace now shows the names of the applied rewrite rules
    1.38 +
    1.39  * Pure: locale specifications now produce predicate definitions
    1.40  according to the body of text (covering assumptions modulo local
    1.41  definitions); predicate "loc_axioms" covers newly introduced text,
    1.42 @@ -72,8 +104,6 @@
    1.43  * simp reduces "m*(n div m) + n mod m" to n, even if the two summands
    1.44  are distributed over a sum of terms;
    1.45  
    1.46 -* the simplifier trace now shows the names of the applied rewrite rules
    1.47 -
    1.48  * induct over a !!-quantified statement (say !!x1..xn):
    1.49    each "case" automatically performs "fix x1 .. xn" with exactly those names.
    1.50