changeset 3671 | 8326f03d667c |
parent 3670 | 9fea3562f8c7 |
child 3697 | c5833dfcc2cc |
--- a/NEWS Thu Sep 11 16:20:56 1997 +0200 +++ b/NEWS Fri Sep 12 10:45:51 1997 +0200 @@ -5,6 +5,9 @@ New in Isabelle???? (DATE ????) ------------------------------- +* added extended adm_tac to simplifier in HOLCF. Is now capable to discharge + adm (%x. P (t x)), where P is chainfinite and t continuous. + * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;