# HG changeset patch
# User wenzelm
# Date 1248640412 -7200
# Node ID 2f3d65d15149f60d380ea66034c58eb8e8d1e7c2
# Parent  87806301a813ed117bb7215f7305fbea22ee6ee1
tacticals FOCUS and FOCUS_PARAMS;

diff -r 87806301a813 -r 2f3d65d15149 NEWS
--- a/NEWS	Sun Jul 26 22:28:31 2009 +0200
+++ b/NEWS	Sun Jul 26 22:33:32 2009 +0200
@@ -118,6 +118,11 @@
 
 *** ML ***
 
+* Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to
+introduce new subgoals and schematic variables.  FOCUS_PARAMS is
+similar, but focuses on the parameter prefix only, leaving subgoal
+premises unchanged.
+
 * Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
 functors have their own ML name space there is no point to mark them
 separately.)  Minor INCOMPATIBILITY.