changeset 8673 | 987ea1a559d0 |
parent 8655 | 16906e600c9a |
child 8705 | a3da5538d924 |
--- 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 ***