# HG changeset patch
# User mueller
# Date 874053951 -7200
# Node ID 8326f03d667cf09e3115f96399629d91a3c46e51
# Parent  9fea3562f8c7d12d6043a832b60e755177635b00
extended adm_tac;

diff -r 9fea3562f8c7 -r 8326f03d667c NEWS
--- 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;