NEWS
changeset 8673 987ea1a559d0
parent 8655 16906e600c9a
child 8705 a3da5538d924
     1.1 --- a/NEWS	Wed Apr 05 21:05:20 2000 +0200
     1.2 +++ b/NEWS	Wed Apr 05 21:06:06 2000 +0200
     1.3 @@ -79,6 +79,11 @@
     1.4  methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' /
     1.5  'induct_tac' (for HOL datatypes);
     1.6  
     1.7 +* simplified (more robust) goal selection of proof methods: 1st goal,
     1.8 +all goals, or explicit goal specifier (tactic emulation); thus 'proof
     1.9 +method scripts' have to be in depth-first order;
    1.10 +
    1.11 +* tuned 'let' syntax: replace 'as' keyword by 'and';
    1.12  
    1.13  
    1.14  *** HOL ***