# HG changeset patch
# User wenzelm
# Date 954961566 -7200
# Node ID 987ea1a559d0f9e2d247ca3fb9d62eb85f1a1c18
# Parent  1f51c411da5a75b3338fbaa5468531c1b26e1fb1
Isar: simplified (more robust) goal selection of proof methods;
Isar: tuned 'let' syntax: replace 'as' keyword by 'and';

diff -r 1f51c411da5a -r 987ea1a559d0 NEWS
--- a/NEWS	Wed Apr 05 21:05:20 2000 +0200
+++ b/NEWS	Wed Apr 05 21:06:06 2000 +0200
@@ -79,6 +79,11 @@
 methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' /
 'induct_tac' (for HOL datatypes);
 
+* simplified (more robust) goal selection of proof methods: 1st goal,
+all goals, or explicit goal specifier (tactic emulation); thus 'proof
+method scripts' have to be in depth-first order;
+
+* tuned 'let' syntax: replace 'as' keyword by 'and';
 
 
 *** HOL ***