--- a/NEWS Wed Jun 28 21:15:02 2000 +0200
+++ b/NEWS Thu Jun 29 12:14:04 2000 +0200
@@ -40,6 +40,13 @@
* Isar: changed syntax of local blocks from {{ }} to { };
+* 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, FOR and ZF the function cla_make_elim will create such rules
+from destruct-rules;
+
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
timing flag supersedes proof_timing and Toplevel.trace;