extended adm_tac;
authormueller
Fri Sep 12 10:45:51 1997 +0200 (1997-09-12)
changeset 36718326f03d667c
parent 3670 9fea3562f8c7
child 3672 56e4365a0c99
extended adm_tac;
NEWS
     1.1 --- a/NEWS	Thu Sep 11 16:20:56 1997 +0200
     1.2 +++ b/NEWS	Fri Sep 12 10:45:51 1997 +0200
     1.3 @@ -5,6 +5,9 @@
     1.4  New in Isabelle???? (DATE ????)
     1.5  -------------------------------
     1.6  
     1.7 +* added extended adm_tac to simplifier in HOLCF. Is now capable to discharge
     1.8 +  adm (%x. P (t x)), where P is chainfinite and t continuous.
     1.9 +
    1.10  * replaced print_goals_ref hook by print_current_goals_fn and
    1.11    result_error_fn;
    1.12