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