# HG changeset patch
# User wenzelm
# Date 953574328 -3600
# Node ID fdbabfbc382955eb8f88357b830ec0ba6368f4d1
# Parent  d534ddf14076afcbe9e2c1654b362865b74de728
improved support for emulating tactic scripts;

diff -r d534ddf14076 -r fdbabfbc3829 NEWS
--- a/NEWS	Mon Mar 20 18:43:37 2000 +0100
+++ b/NEWS	Mon Mar 20 18:45:28 2000 +0100
@@ -61,6 +61,11 @@
 additional print modes to be specified; e.g. "pr(latex)" will print
 proof state according to the Isabelle LaTeX style;
 
+* improved support for emulating tactic scripts, including proof
+methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' /
+'induct_tac' (for HOL datatypes);
+
+
 
 *** HOL ***