improved support for emulating tactic scripts;
authorwenzelm
Mon Mar 20 18:45:28 2000 +0100 (2000-03-20)
changeset 8534fdbabfbc3829
parent 8533 d534ddf14076
child 8535 7428194b39f7
improved support for emulating tactic scripts;
NEWS
     1.1 --- a/NEWS	Mon Mar 20 18:43:37 2000 +0100
     1.2 +++ b/NEWS	Mon Mar 20 18:45:28 2000 +0100
     1.3 @@ -61,6 +61,11 @@
     1.4  additional print modes to be specified; e.g. "pr(latex)" will print
     1.5  proof state according to the Isabelle LaTeX style;
     1.6  
     1.7 +* improved support for emulating tactic scripts, including proof
     1.8 +methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' /
     1.9 +'induct_tac' (for HOL datatypes);
    1.10 +
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14