NEWS
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;