# HG changeset patch
# User krauss
# Date 1163422428 -3600
# Node ID d240748a2cf5488bd3bf233918b2068cee93c8f1
# Parent  cf814e36f788d5c884161779f8b2832acfae6b6b
updated

diff -r cf814e36f788 -r d240748a2cf5 NEWS
--- a/NEWS	Mon Nov 13 13:51:22 2006 +0100
+++ b/NEWS	Mon Nov 13 13:53:48 2006 +0100
@@ -483,6 +483,15 @@
 
 *** HOL ***
 
+* Replaced "auto_term" by the conceptually simpler method "relation",
+which just applies the instantiated termination rule with no further
+simplifications.
+INCOMPATIBILITY: 
+Replace 
+        termination by (auto_term "MYREL")
+with 
+        termination by (relation "MYREL") auto
+
 * Automated termination proofs "by lexicographic_order" are now
 included in the abbreviated function command "fun". No explicit
 "termination" command is necessary anymore.