author | wenzelm |

Fri Jul 24 16:45:20 2020 +0200 (3 weeks ago) | |

changeset 72070 | b17be02a0a11 |

parent 72069 | ebf3ba74bc4c |

child 72071 | d3cad9ecd0cc |

tuned;

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 ***