# HG changeset patch
# User paulson
# Date 962273644 -7200
# Node ID 30d46270a42717508127591981ea202d84ebc94f
# Parent  c6c5b422241f883042e3af2677c4cb469045a1d4
weak elimination rules

diff -r c6c5b422241f -r 30d46270a427 NEWS
--- 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;