# HG changeset patch
# User wenzelm
# Date 1160388513 -7200
# Node ID dab803075c6294a11a45274d15e1df2bd60c25f9
# Parent  b9068bd7255caa18bcbcedae8759194b826c53a7
attribute "symmetric": standardized schematic variables;

diff -r b9068bd7255c -r dab803075c62 NEWS
--- a/NEWS	Mon Oct 09 02:20:11 2006 +0200
+++ b/NEWS	Mon Oct 09 12:08:33 2006 +0200
@@ -434,6 +434,9 @@
 * Provers/induct: support coinduction as well.  See
 src/HOL/Library/Coinductive_List.thy for various examples.
 
+* Attribute "symmetric" produces result with standardized schematic
+variables (index 0).  Potential INCOMPATIBILITY.
+
 * Simplifier: by default the simplifier trace only shows top level rewrites
 now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is
 less danger of being flooded by the trace. The trace indicates where parts