NEWS

 
 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
 
 * calling (stac rew i) now fails if "rew" has no effect on the goal
   [previously, this check worked only if the rewrite rule was unconditional]
-
+  Now rew can involve either definitions or equalities (either == or =).
 
 *** ZF ***
 
 * theory Main includes everything;
 

 
 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
 
 * calling (stac rew i) now fails if "rew" has no effect on the goal
   [previously, this check worked only if the rewrite rule was unconditional]
+  Now rew can involve either definitions or equalities (either == or =).
 
 * case_tac provided for compatibility with HOL
     (like the old excluded_middle_tac, but with subgoals swapped)