Isar: simplified (more robust) goal selection of proof methods;
authorwenzelm
Wed Apr 05 21:06:06 2000 +0200 (2000-04-05)
changeset 8673987ea1a559d0
parent 8672 1f51c411da5a
child 8674 ac6c028e0249
Isar: simplified (more robust) goal selection of proof methods;
Isar: tuned 'let' syntax: replace 'as' keyword by 'and';
NEWS
     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 ***