# HG changeset patch # User paulson # Date 963578795 -7200 # Node ID 5d9f02e7556900519288ca896edfe9f39728122d # Parent f0c2b71db81bf57b50a2de77dceba97864f46b1b AddIffs diff -r f0c2b71db81b -r 5d9f02e75569 NEWS --- a/NEWS Fri Jul 14 13:57:00 2000 +0200 +++ b/NEWS Fri Jul 14 14:46:35 2000 +0200 @@ -41,12 +41,15 @@ * Isar: changed syntax of local blocks from {{ }} to { }; +* FOL, ZF: AddIffs now available, giving theorems of the form P<->Q to the + simplifier and classical reasoner simultaneously; + * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g. [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W use instead the strong form, [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W In HOL, FOL and ZF the function cla_make_elim will create such rules -from destruct-rules. +from destruct-rules; * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global timing flag supersedes proof_timing and Toplevel.trace;