tuned;
authorwenzelm
Fri Jul 24 16:45:20 2020 +0200 (3 weeks ago)
changeset 72070b17be02a0a11
parent 72069 ebf3ba74bc4c
child 72071 d3cad9ecd0cc
tuned;
NEWS
     1.1 --- a/NEWS	Fri Jul 24 15:20:35 2020 +0200
     1.2 +++ b/NEWS	Fri Jul 24 16:45:20 2020 +0200
     1.3 @@ -37,6 +37,12 @@
     1.4  * Session HOL-Examples contains notable examples for Isabelle/HOL
     1.5  (former entries of HOL-Isar_Examples, HOL-ex etc.).
     1.6  
     1.7 +* Simproc "defined_all" and rewrite rule "subst_all" perform more
     1.8 +aggressive substitution with variables from assumptions.
     1.9 +INCOMPATIBILITY, consider repairing proofs locally like this:
    1.10 +
    1.11 +  supply subst_all [simp del] [[simproc del: defined_all]]
    1.12 +
    1.13  * Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
    1.14  on datatypes to "False" if either side is a proper subexpression of the
    1.15  other (for any datatype with a reasonable size function).
    1.16 @@ -85,26 +91,17 @@
    1.17  into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
    1.18  INCOMPATIBILITY.
    1.19  
    1.20 -* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer"
    1.21 -commands are in working order again, as opposed to outputting
    1.22 -"GaveUp" on nearly all problems.
    1.23 -
    1.24 -* Simproc defined_all and rewrite rule subst_all perform
    1.25 -more aggressive substitution with variables from assumptions.
    1.26 -INCOMPATIBILITY, use something like
    1.27 -"supply subst_all [simp del] [[simproc del: defined_all]]"
    1.28 -to leave fragile proofs unaffected.
    1.29 +* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
    1.30 +are in working order again, as opposed to outputting "GaveUp" on nearly
    1.31 +all problems.
    1.32  
    1.33  
    1.34  *** FOL ***
    1.35  
    1.36  * Added the "at most 1" quantifier, Uniq, as in HOL.
    1.37  
    1.38 -* Simproc defined_all and rewrite rule subst_all perform
    1.39 -more aggressive substitution with variables from assumptions.
    1.40 -INCOMPATIBILITY, use something like
    1.41 -"supply subst_all [simp del] [[simproc del: defined_all]]"
    1.42 -to leave fragile proofs unaffected.
    1.43 +* Simproc "defined_all" and rewrite rule "subst_all" have been changed
    1.44 +as in HOL.
    1.45  
    1.46  
    1.47  *** ML ***