# HG changeset patch
# User wenzelm
# Date 1137351537 -3600
# Node ID 83f50ac6ddcb1e9e93df1e6187667880d0eab2e1
# Parent  8ae076ee5e1954f251a0df1265f64a20967c911d
* Classical:  optional weight for attributes;
* HOL: prefer ex1I over ex_ex1I in single-step reasoning;

diff -r 8ae076ee5e19 -r 83f50ac6ddcb NEWS
--- a/NEWS	Sun Jan 15 19:58:56 2006 +0100
+++ b/NEWS	Sun Jan 15 19:58:57 2006 +0100
@@ -225,8 +225,14 @@
 attribute; classical elim/dest rules are now treated uniformly when
 manipulating the claset.
 
-* Provers/classical: stricter checks to ensure that supplied intro, dest and 
-elim rules are well-formed; dest and elim rules must have at least one premise.
+* Provers/classical: stricter checks to ensure that supplied intro,
+dest and elim rules are well-formed; dest and elim rules must have at
+least one premise.
+
+* Provers/classical: attributes dest/elim/intro take an optional
+weight argument for the rule (just as the Pure versions); weights are
+ignored by automated rules, but determines the search order of single
+rule steps.
 
 * Syntax: input syntax now supports dummy variable binding "%_. b",
 where the body does not mention the bound variable.  Note that dummy
@@ -242,6 +248,9 @@
 
 *** HOL ***
 
+* Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
+'rule' method.
+
 * Alternative iff syntax "A <-> B" for equality on bool (with priority
 25 like -->); output depends on the "iff" print_mode, the default is
 "A = B" (with priority 50).